>PhoX> Sort term. Sort term defined >PhoX> Cst A : term term prop. A : term term prop >PhoX> Cst B : term term prop. B : term term prop >PhoX> Cst C : term term prop. C : term term prop >PhoX> Cst D : term term prop. D : term term prop >PhoX> theorem numero1 e a x ( A a x B e x ) a b x ( >PhoX> C b x A a x ) e a ( B e a D e a ) e a >PhoX> x ( C a x D e x ). Here is the goal: goal 1/1 e a x:(A a) B e x a b x:(C b) A a x e,a (B e a D e a) e a x:(C a) D e x %PhoX% intro. 1 goal created. goal 1/1 H := e a x:(A a) B e x a b x:(C b) A a x e,a (B e a D e a) e a x:(C a) D e x %PhoX% lefts H. 1 goal created. goal 1/1 H0 := e,a (B e a D e a) H := e a x:(A a) B e x H1 := a b x:(C b) A a x e a x:(C a) D e x %PhoX% intro 1. 1 goal created. goal 1/1 H0 := e0,a (B e0 a D e0 a) H := e0 a x:(A a) B e0 x H1 := a b x:(C b) A a x a x:(C a) D e x %PhoX% apply H with e. 1 goal created. goal 1/1 H0 := e0,a (B e0 a D e0 a) H := e0 a x:(A a) B e0 x H1 := a b x:(C b) A a x G := a x:(A a) B e x a x:(C a) D e x %PhoX% elim G. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x:(A a0) B e0 x H1 := a0 b x:(C b) A a0 x G := a0 x:(A a0) B e x H2 := x:(A a) B e x a0 x:(C a0) D e x %PhoX% apply H1 with a. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x:(A a0) B e0 x H1 := a0 b x:(C b) A a0 x G := a0 x:(A a0) B e x H2 := x:(A a) B e x G0 := b x:(C b) A a x a0 x:(C a0) D e x %PhoX% elim G0. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x:(A a0) B e0 x H1 := a0 b0 x:(C b0) A a0 x G := a0 x:(A a0) B e x H2 := x:(A a) B e x G0 := b0 x:(C b0) A a x H3 := x:(C b) A a x a0 x:(C a0) D e x %PhoX% intro. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x:(A a0) B e0 x H1 := a0 b0 x:(C b0) A a0 x G := a0 x:(A a0) B e x H2 := x:(A a) B e x G0 := b0 x:(C b0) A a x H3 := x:(C b) A a x x:(C ?1) D e x %PhoX% instance ?1 b. Here is the goal: goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x:(A a0) B e0 x H1 := a0 b0 x:(C b0) A a0 x G := a0 x:(A a0) B e x H2 := x:(A a) B e x G0 := b0 x:(C b0) A a x H3 := x:(C b) A a x x:(C b) D e x %PhoX% intro. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 C b x D e x %PhoX% apply H2 with x. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 G1 := A a x B e x C b x D e x %PhoX% apply H3 with x. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 G1 := A a x B e x G2 := C b x A a x C b x D e x %PhoX% apply H0 with e. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 G1 := A a x B e x G2 := C b x A a x G3 := a0:(B e) D e a0 C b x D e x %PhoX% apply G3 with x. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 G1 := A a x B e x G2 := C b x A a x G3 := a0:(B e) D e a0 G4 := B e x D e x C b x D e x %PhoX% intro. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 G1 := A a x B e x G2 := C b x A a x G3 := a0:(B e) D e a0 G4 := B e x D e x H4 := C b x D e x %PhoX% elim G4. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 G1 := A a x B e x G2 := C b x A a x G3 := a0:(B e) D e a0 G4 := B e x D e x H4 := C b x B e x %PhoX% elim G1. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 G1 := A a x B e x G2 := C b x A a x G3 := a0:(B e) D e a0 G4 := B e x D e x H4 := C b x A a x %PhoX% elim G2. 1 goal created. goal 1/1 H0 := e0,a0 (B e0 a0 D e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(C b0) A a0 x0 G := a0 x0:(A a0) B e x0 H2 := x0:(A a) B e x0 G0 := b0 x0:(C b0) A a x0 H3 := x0:(C b) A a x0 G1 := A a x B e x G2 := C b x A a x G3 := a0:(B e) D e a0 G4 := B e x D e x H4 := C b x C b x %PhoX% axiom H4. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero1 = e x x0:(A x) B e x0 a b x:(C b) A a x e,a (B e a D e a) e a x:(C a) D e x : theorem >PhoX> theorem numero2 e a x ( A a x B e x ) a b x ( >PhoX> B b x D a x ) e a ( C e a A e a ) e a >PhoX> x ( C a x D e x ). Here is the goal: goal 1/1 e a x:(A a) B e x a b x:(B b) D a x e,a (C e a A e a) e a x:(C a) D e x %PhoX% intro. 1 goal created. goal 1/1 H := e a x:(A a) B e x a b x:(B b) D a x e,a (C e a A e a) e a x:(C a) D e x %PhoX% lefts H. 1 goal created. goal 1/1 H0 := e,a (C e a A e a) H := e a x:(A a) B e x H1 := a b x:(B b) D a x e a x:(C a) D e x %PhoX% intro. 1 goal created. goal 1/1 H0 := e0,a (C e0 a A e0 a) H := e0 a x:(A a) B e0 x H1 := a b x:(B b) D a x a x:(C a) D e x %PhoX% apply H1 with e. 1 goal created. goal 1/1 H0 := e0,a (C e0 a A e0 a) H := e0 a x:(A a) B e0 x H1 := a b x:(B b) D a x G := b x:(B b) D e x a x:(C a) D e x %PhoX% elim G. 1 goal created. goal 1/1 H0 := e0,a (C e0 a A e0 a) H := e0 a x:(A a) B e0 x H1 := a b0 x:(B b0) D a x G := b0 x:(B b0) D e x H2 := x:(B b) D e x a x:(C a) D e x %PhoX% apply H with b. 1 goal created. goal 1/1 H0 := e0,a (C e0 a A e0 a) H := e0 a x:(A a) B e0 x H1 := a b0 x:(B b0) D a x G := b0 x:(B b0) D e x H2 := x:(B b) D e x G0 := a x:(A a) B b x a x:(C a) D e x %PhoX% elim G0. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x:(A a0) B e0 x H1 := a0 b0 x:(B b0) D a0 x G := b0 x:(B b0) D e x H2 := x:(B b) D e x G0 := a0 x:(A a0) B b x H3 := x:(A a) B b x a0 x:(C a0) D e x %PhoX% intro. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x:(A a0) B e0 x H1 := a0 b0 x:(B b0) D a0 x G := b0 x:(B b0) D e x H2 := x:(B b) D e x G0 := a0 x:(A a0) B b x H3 := x:(A a) B b x x:(C ?1) D e x %PhoX% instance ?1 a. Here is the goal: goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x:(A a0) B e0 x H1 := a0 b0 x:(B b0) D a0 x G := b0 x:(B b0) D e x H2 := x:(B b) D e x G0 := a0 x:(A a0) B b x H3 := x:(A a) B b x x:(C a) D e x %PhoX% intro 2. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(B b0) D a0 x0 G := b0 x0:(B b0) D e x0 H2 := x0:(B b) D e x0 G0 := a0 x0:(A a0) B b x0 H3 := x0:(A a) B b x0 H4 := C a x D e x %PhoX% apply H2 with x. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(B b0) D a0 x0 G := b0 x0:(B b0) D e x0 H2 := x0:(B b) D e x0 G0 := a0 x0:(A a0) B b x0 H3 := x0:(A a) B b x0 H4 := C a x G1 := B b x D e x D e x %PhoX% apply H3 with x. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(B b0) D a0 x0 G := b0 x0:(B b0) D e x0 H2 := x0:(B b) D e x0 G0 := a0 x0:(A a0) B b x0 H3 := x0:(A a) B b x0 H4 := C a x G1 := B b x D e x G2 := A a x B b x D e x %PhoX% apply H0 with a. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(B b0) D a0 x0 G := b0 x0:(B b0) D e x0 H2 := x0:(B b) D e x0 G0 := a0 x0:(A a0) B b x0 H3 := x0:(A a) B b x0 H4 := C a x G1 := B b x D e x G2 := A a x B b x G3 := a0:(C a) A a a0 D e x %PhoX% apply G3 with x. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(B b0) D a0 x0 G := b0 x0:(B b0) D e x0 H2 := x0:(B b) D e x0 G0 := a0 x0:(A a0) B b x0 H3 := x0:(A a) B b x0 H4 := C a x G1 := B b x D e x G2 := A a x B b x G3 := a0:(C a) A a a0 G4 := C a x A a x D e x %PhoX% elim G1. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(B b0) D a0 x0 G := b0 x0:(B b0) D e x0 H2 := x0:(B b) D e x0 G0 := a0 x0:(A a0) B b x0 H3 := x0:(A a) B b x0 H4 := C a x G1 := B b x D e x G2 := A a x B b x G3 := a0:(C a) A a a0 G4 := C a x A a x B b x %PhoX% elim G2. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(B b0) D a0 x0 G := b0 x0:(B b0) D e x0 H2 := x0:(B b) D e x0 G0 := a0 x0:(A a0) B b x0 H3 := x0:(A a) B b x0 H4 := C a x G1 := B b x D e x G2 := A a x B b x G3 := a0:(C a) A a a0 G4 := C a x A a x A a x %PhoX% elim G4. 1 goal created. goal 1/1 H0 := e0,a0 (C e0 a0 A e0 a0) H := e0 a0 x0:(A a0) B e0 x0 H1 := a0 b0 x0:(B b0) D a0 x0 G := b0 x0:(B b0) D e x0 H2 := x0:(B b) D e x0 G0 := a0 x0:(A a0) B b x0 H3 := x0:(A a) B b x0 H4 := C a x G1 := B b x D e x G2 := A a x B b x G3 := a0:(C a) A a a0 G4 := C a x A a x C a x %PhoX% axiom H4. 0 goal created. %PhoX% save. Building proof .... Typing proof .... Verifying proof .... Saving proof .... numero2 = e x x0:(A x) B e x0 a x x0:(B x) D a x0 e,a (C e a A e a) e a x:(C a) D e x : theorem bye