```>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
```