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

>PhoX> theorem numero1  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 goals created.

goal 2/2
x A x  x B x  x (A x  B x)

goal 1/2
x (A x  B x)  x A x  x B x

%PhoX% intro 2.
2 goals created.

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

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
0 goal created.

goal 2/2
x A x  x B x  x (A x  B x)

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
0 goal created.

goal 1/1
x A x  x B x  x (A x  B x)

%PhoX% intro 3.
2 goals created.

goal 2/2
H := x0 A x0  x0 B x0
B x

goal 1/2
H := x0 A x0  x0 B x0
A x

%PhoX% elim H.
0 goal created.

goal 1/1
H := x0 A x0  x0 B x0
B x

%PhoX% elim H.
0 goal created.

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

>PhoX> Sort term.
This symbol already exists (ignored).
Sort term defined
>PhoX> Cst A : term  prop.
This symbol already exists (ignored).
A : term  prop
>PhoX> Cst B :  term  prop.
This symbol already exists (ignored).
B : term  prop

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

%PhoX% intro 2.
2 goals created.

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

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

%PhoX% elim H.
1 goal created.

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

%PhoX% left H0.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% left H0.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% axiom H1.
0 goal created.

%PhoX% save numero2.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
numero2 = x:A  B x  x A x  x B x : theorem

>PhoX> Sort term.
This symbol already exists (ignored).
Sort term defined
>PhoX> Cst A : term  prop.
This symbol already exists (ignored).
A : term  prop
>PhoX> Cst B1 : prop.
B1 : prop

>PhoX> theorem numero3   x ( A x  B1)  ( x A x  B1).
Here is the goal:
goal 1/1
x:A  B1  x A x  B1

%PhoX% intro.
2 goals created.

goal 2/2
x A x  B1  x:A  B1

goal 1/2
x:A  B1  x A x  B1

%PhoX% intro 2.
2 goals created.

goal 2/3
H := x:A  B1
B1

goal 1/3
H := x:A  B1
x A x

%PhoX% elim H.
1 goal created.

goal 1/3
H := x0:A  B1
H0 := A x  B1
x0 A x0

%PhoX% left H0.
1 goal created.

goal 1/3
H := x0:A  B1
H0 := A x
H1 := B1
x0 A x0

%PhoX% intro.
1 goal created.

goal 1/3
H := x0:A  B1
H0 := A x
H1 := B1
A ?1

%PhoX% axiom H0.
0 goal created.

goal 2/2
x A x  B1  x:A  B1

goal 1/2
H := x:A  B1
B1

%PhoX% elim H.
1 goal created.

goal 1/2
H := x0:A  B1
H0 := A x  B1
B1

%PhoX% left H0.
1 goal created.

goal 1/2
H := x0:A  B1
H0 := A x
H1 := B1
B1

%PhoX% axiom H1.
0 goal created.

goal 1/1
x A x  B1  x:A  B1

%PhoX% intro.
1 goal created.

goal 1/1
H := x A x  B1
x:A  B1

%PhoX% left H.
1 goal created.

goal 1/1
H := x A x
H0 := B1
x:A  B1

%PhoX% elim H.
1 goal created.

goal 1/1
H := x0 A x0
H0 := B1
H1 := A x
x0:A  B1

%PhoX% intro 2.
2 goals created.

goal 2/2
H := x0 A x0
H0 := B1
H1 := A x
B1

goal 1/2
H := x0 A x0
H0 := B1
H1 := A x
A ?2

%PhoX% axiom H1.
0 goal created.

goal 1/1
H := x0 A x0
H0 := B1
H1 := A x
B1

%PhoX% axiom H0.
0 goal created.

%PhoX% save numero3.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
numero3 = x:A  B1  x A x  B1 : theorem

>PhoX> Sort term.
This symbol already exists (ignored).
Sort term defined
>PhoX> Cst A : term  prop.
This symbol already exists (ignored).
A : term  prop
>PhoX> Cst B :  term  prop.
This symbol already exists (ignored).
B : term  prop

>PhoX> theorem numero4  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 goals created.

goal 2/2
x A x  x B x  x (A x  B x)

goal 1/2
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)
x A x  x B x

%PhoX% elim H.
1 goal created.

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

%PhoX% left H0.
2 goals created.

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

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

%PhoX% intro r.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

goal 2/2
x A x  x B x  x (A x  B x)

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

%PhoX% intro l.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

goal 1/1
x A x  x B x  x (A x  B x)

%PhoX% intro.
1 goal created.

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

%PhoX% left H.
2 goals created.

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

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro.
1 goal created.

goal 1/2
H := x0 B x0
H0 := B x
A ?3  B ?3

%PhoX% intro r.
1 goal created.

goal 1/2
H := x0 B x0
H0 := B x
B ?3

%PhoX% axiom H0.
0 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro.
1 goal created.

goal 1/1
H := x0 A x0
H0 := A x
A ?4  B ?4

%PhoX% intro l.
1 goal created.

goal 1/1
H := x0 A x0
H0 := A x
A ?4

%PhoX% axiom H0.
0 goal created.

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

>PhoX> Sort term.
This symbol already exists (ignored).
Sort term defined
>PhoX> Cst A : term  prop.
This symbol already exists (ignored).
A : term  prop
>PhoX> Cst B :  term  prop.
This symbol already exists (ignored).
B : term  prop
>PhoX> Cst A1 : prop.
A1 : prop
>PhoX> Cst B1 : prop.
This symbol already exists (ignored).
B1 : prop

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

%PhoX% intro 2.
1 goal created.

goal 1/1
H := x0 A x0  x0 B x0
A x  B x

%PhoX% left H.
2 goals created.

goal 2/2
H := x0 A x0
A x  B x

goal 1/2
H := x0 B x0
A x  B x

%PhoX% intro r.
1 goal created.

goal 1/2
H := x0 B x0
B x

%PhoX% elim H.
0 goal created.

goal 1/1
H := x0 A x0
A x  B x

%PhoX% intro l.
1 goal created.

goal 1/1
H := x0 A x0
A x

%PhoX% elim H.
0 goal created.

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

>PhoX> theorem numero7 x(A1  B x)(A1 x B x).
Here is the goal:
goal 1/1
x (A1  B x)  (A1  x B x)

%PhoX% intros.
2 goals created.

goal 2/2
(A1  x B x)  x (A1  B x)

goal 1/2
x (A1  B x)  A1  x B x

%PhoX% intro 3.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

goal 1/1
(A1  x B x)  x (A1  B x)

%PhoX% intro 3.
1 goal created.

goal 1/1
H := A1  x0 B x0
H0 := A1
B x

%PhoX% elim H.
1 goal created.

goal 1/1
H := A1  x0 B x0
H0 := A1
A1

%PhoX% axiom H0.
0 goal created.

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

>PhoX> theorem numero8 x(A x  B1)(x A x  B1).
Here is the goal:
goal 1/1
x:A  B1  (x A x  B1)

%PhoX% intros.
2 goals created.

goal 2/2
(x A x  B1)  x:A  B1

goal 1/2
x:A  B1  x A x  B1

%PhoX% intros.
1 goal created.

goal 1/2
H := x:A  B1
H0 := x A x
B1

%PhoX% left H0.
1 goal created.

goal 1/2
H := x0:A  B1
H0 := A x
B1

%PhoX% elim H.
1 goal created.

goal 1/2
H := x0:A  B1
H0 := A x
A ?1

%PhoX% axiom H0.
0 goal created.

goal 1/1
(x A x  B1)  x:A  B1

%PhoX% intros.
1 goal created.

goal 1/1
H := x0 A x0  B1
H0 := A x
B1

%PhoX% elim H.
1 goal created.

goal 1/1
H := x0 A x0  B1
H0 := A x
x0 A x0

%PhoX% intro.
1 goal created.

goal 1/1
H := x0 A x0  B1
H0 := A x
A ?2

%PhoX% axiom H0.
0 goal created.

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

bye
```