>PhoX> Cst a : prop.
a : prop
>PhoX> Cst b : prop.
b : prop
>PhoX> Cst c : prop.
c : prop
>PhoX> Cst d : prop.
d : prop

>PhoX> theorem numero1 (a  b)  ( a   b).
Here is the goal:
goal 1/1
    a  b   a   b

%PhoX% intro 2.
2 goals created.

goal 2/2
H := a  b
     b   a

goal 1/2
H := a  b
     a   b

%PhoX% intro 2.
1 goal created.

goal 1/2
H := a  b
H0 :=  a
H1 := b
    False

%PhoX% left H.
1 goal created.

goal 1/2
H0 :=  a
H1 := b
H := a  b
H2 := b  a
    False

%PhoX% elim H0.
1 goal created.

goal 1/2
H0 :=  a
H1 := b
H := a  b
H2 := b  a
    a

%PhoX% elim H2.
1 goal created.

goal 1/2
H0 :=  a
H1 := b
H := a  b
H2 := b  a
    b

%PhoX% axiom H1.
0 goal created.

goal 1/1
H := a  b
     b   a

%PhoX% intro 2.
1 goal created.

goal 1/1
H := a  b
H0 :=  b
H1 := a
    False

%PhoX% left H.
1 goal created.

goal 1/1
H0 :=  b
H1 := a
H := a  b
H2 := b  a
    False

%PhoX% elim H0.
1 goal created.

goal 1/1
H0 :=  b
H1 := a
H := a  b
H2 := b  a
    b

%PhoX% elim H.
1 goal created.

goal 1/1
H0 :=  b
H1 := a
H := a  b
H2 := b  a
    a

%PhoX% axiom H1.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero1 = a  b   a   b : theorem


>PhoX> theorem numero2 (a  b)  (c  d)  (a  c  b  d).
Here is the goal:
goal 1/1
    a  b  c  d  a  c  b  d

%PhoX% intro 3.
2 goals created.

goal 2/2
H := a  b
H0 := c  d
    b  d  a  c

goal 1/2
H := a  b
H0 := c  d
    a  c  b  d

%PhoX% intro 2.
2 goals created.

goal 2/3
H := a  b
H0 := c  d
H1 := a  c
    d

goal 1/3
H := a  b
H0 := c  d
H1 := a  c
    b

%PhoX% left H.
1 goal created.

goal 1/3
H0 := c  d
H1 := a  c
H := a  b
H2 := b  a
    b

%PhoX% left H1.
1 goal created.

goal 1/3
H0 := c  d
H := a  b
H2 := b  a
H1 := a
H3 := c
    b

%PhoX% elim H.
1 goal created.

goal 1/3
H0 := c  d
H := a  b
H2 := b  a
H1 := a
H3 := c
    a

%PhoX% axiom H1.
0 goal created.

goal 2/2
H := a  b
H0 := c  d
    b  d  a  c

goal 1/2
H := a  b
H0 := c  d
H1 := a  c
    d

%PhoX% left H0.
1 goal created.

goal 1/2
H := a  b
H1 := a  c
H0 := c  d
H2 := d  c
    d

%PhoX% left H1.
1 goal created.

goal 1/2
H := a  b
H0 := c  d
H2 := d  c
H1 := a
H3 := c
    d

%PhoX% elim H0.
1 goal created.

goal 1/2
H := a  b
H0 := c  d
H2 := d  c
H1 := a
H3 := c
    c

%PhoX% axiom H3.
0 goal created.

goal 1/1
H := a  b
H0 := c  d
    b  d  a  c

%PhoX% intro 2.
2 goals created.

goal 2/2
H := a  b
H0 := c  d
H1 := b  d
    c

goal 1/2
H := a  b
H0 := c  d
H1 := b  d
    a

%PhoX% left H.
1 goal created.

goal 1/2
H0 := c  d
H1 := b  d
H := a  b
H2 := b  a
    a

%PhoX% left H1.
1 goal created.

goal 1/2
H0 := c  d
H := a  b
H2 := b  a
H1 := b
H3 := d
    a

%PhoX% elim H2.
1 goal created.

goal 1/2
H0 := c  d
H := a  b
H2 := b  a
H1 := b
H3 := d
    b

%PhoX% axiom H1.
0 goal created.

goal 1/1
H := a  b
H0 := c  d
H1 := b  d
    c

%PhoX% left H0.
1 goal created.

goal 1/1
H := a  b
H1 := b  d
H0 := c  d
H2 := d  c
    c

%PhoX% left H1.
1 goal created.

goal 1/1
H := a  b
H0 := c  d
H2 := d  c
H1 := b
H3 := d
    c

%PhoX% elim H2.
1 goal created.

goal 1/1
H := a  b
H0 := c  d
H2 := d  c
H1 := b
H3 := d
    d

%PhoX% axiom H3.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero2 = a  b  c  d  a  c  b  d : theorem


>PhoX> theorem numero3 (a  b)  (c  d)  (a  c  b  d).
Here is the goal:
goal 1/1
    a  b  c  d  a  c  b  d

%PhoX% intro 2.
1 goal created.

goal 1/1
H := a  b
H0 := c  d
    a  c  b  d

%PhoX% left H.
1 goal created.

goal 1/1
H0 := c  d
H := a  b
H1 := b  a
    a  c  b  d

%PhoX% left H0.
1 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    a  c  b  d

%PhoX% intro.
2 goals created.

goal 2/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    b  d  a  c

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    a  c  b  d

%PhoX% intro.
1 goal created.

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := a  c
    b  d

%PhoX% left H3.
2 goals created.

goal 2/3
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := a
    b  d

goal 1/3
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := c
    b  d

%PhoX% intro r.
1 goal created.

goal 1/3
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := c
    d

%PhoX% trivial.
0 goal created.

goal 2/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    b  d  a  c

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := a
    b  d

%PhoX% intro l.
1 goal created.

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := a
    b

%PhoX% trivial.
0 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    b  d  a  c

%PhoX% intro.
1 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := b  d
    a  c

%PhoX% left H3.
2 goals created.

goal 2/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := b
    a  c

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := d
    a  c

%PhoX% intro r.
1 goal created.

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := d
    c

%PhoX% trivial.
0 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := b
    a  c

%PhoX% intro l.
1 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := b
    a

%PhoX% trivial.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero3 = a  b  c  d  a  c  b  d : theorem


>PhoX> theorem numero4 (a  b)  (c  d)  ((a  c)  (b  d)).
Here is the goal:
goal 1/1
    a  b  c  d  (a  c)  (b  d)

%PhoX% intro 2.
1 goal created.

goal 1/1
H := a  b
H0 := c  d
    (a  c)  (b  d)

%PhoX% left H.
1 goal created.

goal 1/1
H0 := c  d
H := a  b
H1 := b  a
    (a  c)  (b  d)

%PhoX% left H0.
1 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    (a  c)  (b  d)

%PhoX% intro.
2 goals created.

goal 2/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    (b  d)  a  c

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    (a  c)  b  d

%PhoX% intro 2.
1 goal created.

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := a  c
H4 := b
    d

%PhoX% elim H0.
1 goal created.

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := a  c
H4 := b
    c

%PhoX% elim H3.
1 goal created.

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := a  c
H4 := b
    a

%PhoX% elim H1.
1 goal created.

goal 1/2
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := a  c
H4 := b
    b

%PhoX% axiom H4.
0 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
    (b  d)  a  c

%PhoX% intro 2.
1 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := b  d
H4 := a
    c

%PhoX% elim H2.
1 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := b  d
H4 := a
    d

%PhoX% elim H3.
1 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := b  d
H4 := a
    b

%PhoX% elim H.
1 goal created.

goal 1/1
H := a  b
H1 := b  a
H0 := c  d
H2 := d  c
H3 := b  d
H4 := a
    a

%PhoX% axiom H4.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero4 = a  b  c  d  (a  c)  (b  d) : theorem

>PhoX> Sort term.
Sort term defined
>PhoX> Cst A : term  prop.
A : term  prop
>PhoX> Cst B : term  prop.
B : term  prop

>PhoX> theorem numero5 x (A x  B x)  (x A x  x B x). Here is the goal:
goal 1/1
    x (A x  B x)  x A x  x B x


%PhoX% intro 4.
2 goals created.

goal 2/2
H := x0 (A x0  B x0)
H0 := x0 B x0
    A x

goal 1/2
H := x0 (A x0  B x0)
H0 := x0 A x0
    B x

%PhoX% elim H.
1 goal created.

goal 1/2
H := x0 (A x0  B x0)
H0 := x0 A x0
    A x

%PhoX% elim H0.
0 goal created.

goal 1/1
H := x0 (A x0  B x0)
H0 := x0 B x0
    A x

%PhoX% elim H.
1 goal created.

goal 1/1
H := x0 (A x0  B x0)
H0 := x0 B x0
    B x

%PhoX% elim H0.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero5 = x (A x  B x)  x A x  x B x : theorem


>PhoX> theorem numero6 x (A x  B x)  (x A x  x B x). Here is the goal:
goal 1/1
    x (A x  B x)  x A x  x B x


%PhoX% intro 2.
2 goals created.

goal 2/2
H := x (A x  B x)
    x B x  x A x

goal 1/2
H := x (A x  B x)
    x A x  x B x

%PhoX% intro.
1 goal created.

goal 1/2
H := x (A x  B x)
H0 := x A x
    x B x

%PhoX% elim H0.
1 goal created.

goal 1/2
H := x0 (A x0  B x0)
H0 := x0 A x0
H1 := A x
    x0 B x0

%PhoX% elim H.
1 goal created.

goal 1/2
H := x0 (A x0  B x0)
H0 := x0 A x0
H1 := A x
H2 := A ?1  B ?1
H3 := B ?1  A ?1
    x0 B x0

%PhoX% intro.
1 goal created.

goal 1/2
H := x0 (A x0  B x0)
H0 := x0 A x0
H1 := A x
H2 := A ?1  B ?1
H3 := B ?1  A ?1
    B ?2

%PhoX% elim H2.
1 goal created.

goal 1/2
H := x0 (A x0  B x0)
H0 := x0 A x0
H1 := A x
H2 := A ?2  B ?2
H3 := B ?2  A ?2
    A ?2

%PhoX% axiom H1.
0 goal created.

goal 1/1
H := x (A x  B x)
    x B x  x A x

%PhoX% intro.
1 goal created.

goal 1/1
H := x (A x  B x)
H0 := x B x
    x A x

%PhoX% elim H0.
1 goal created.

goal 1/1
H := x0 (A x0  B x0)
H0 := x0 B x0
H1 := B x
    x0 A x0

%PhoX% elim H.
1 goal created.

goal 1/1
H := x0 (A x0  B x0)
H0 := x0 B x0
H1 := B x
H2 := A ?3  B ?3
H3 := B ?3  A ?3
    x0 A x0

%PhoX% intro.
1 goal created.

goal 1/1
H := x0 (A x0  B x0)
H0 := x0 B x0
H1 := B x
H2 := A ?3  B ?3
H3 := B ?3  A ?3
    A ?4

%PhoX% elim H3.
1 goal created.

goal 1/1
H := x0 (A x0  B x0)
H0 := x0 B x0
H1 := B x
H2 := A ?4  B ?4
H3 := B ?4  A ?4
    B ?4

%PhoX% axiom H1.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero6 = x (A x  B x)  x A x  x B x : theorem

bye