>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