>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)(A1x 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