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

>PhoX> theorem numero4 ((a  b  c)   c)  (((a  c  c)  ((b

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

%PhoX% intros.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intros.
1 goal created.

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

%PhoX% elim H0.
2 goals created.

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

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

%PhoX% intros.
1 goal created.

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

%PhoX% trivial.
0 goal created.

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

%PhoX% intros.
1 goal created.

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

%PhoX% trivial.
0 goal created.

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

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

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

%PhoX% intro.
2 goals created.

goal 2/2
(a  b)  (a  c)  a  b  c

goal 1/2
(a  b  c)  (a  b)  (a  c)

%PhoX% intro 2.
2 goals created.

goal 2/3
H := a  b  c
a  c

goal 1/3
H := a  b  c
a  b

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

goal 2/2
(a  b)  (a  c)  a  b  c

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

goal 1/1
(a  b)  (a  c)  a  b  c

%PhoX% intro 3.
2 goals created.

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

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

%PhoX% left H.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

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

%PhoX% left H.
1 goal created.

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

%PhoX% elim H1.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

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

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

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

%PhoX% intro.
2 goals created.

goal 2/2
(a  c)  (b  c)  a  b  c

goal 1/2
(a  b  c)  (a  c)  (b  c)

%PhoX% intro.
1 goal created.

goal 1/2
H := a  b  c
(a  c)  (b  c)

%PhoX% by_absurd.
1 goal created.

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

%PhoX% rewrite_hyp H0 disjunction.demorgan.
1 goal created.

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

%PhoX% left H0.
1 goal created.

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

%PhoX% rewrite_hyp H0 arrow.demorgan.
1 goal created.

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

%PhoX% left H0.
1 goal created.

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

%PhoX% rewrite_hyp H1 arrow.demorgan.
1 goal created.

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

%PhoX% left H1.
1 goal created.

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

%PhoX% intro 2.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% trivial.
0 goal created.

goal 1/1
(a  c)  (b  c)  a  b  c

%PhoX% intro 2.
1 goal created.

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

%PhoX% left H0.
1 goal created.

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

%PhoX% left H.
2 goals created.

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

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

%PhoX% trivial.
0 goal created.

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

%PhoX% trivial.
0 goal created.

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

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

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

%PhoX% intro.
2 goals created.

goal 2/2
(a  c)  (b  c)  a  b  c

goal 1/2
a  b  c  (a  c)  (b  c)

%PhoX% intro 2.
2 goals created.

goal 2/3
H := a  b  c
b  c

goal 1/3
H := a  b  c
a  c

%PhoX% left H.
2 goals created.

goal 2/4
H := a  b
a  c

goal 1/4
H := c
a  c

%PhoX% trivial.
0 goal created.

goal 3/3
(a  c)  (b  c)  a  b  c

goal 2/3
H := a  b  c
b  c

goal 1/3
H := a  b
a  c

%PhoX% left H.
1 goal created.

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

%PhoX% trivial.
0 goal created.

goal 2/2
(a  c)  (b  c)  a  b  c

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

%PhoX% left H.
2 goals created.

goal 2/3
H := a  b
b  c

goal 1/3
H := c
b  c

%PhoX% trivial.
0 goal created.

goal 2/2
(a  c)  (b  c)  a  b  c

goal 1/2
H := a  b
b  c

%PhoX% left H.
1 goal created.

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

%PhoX% trivial.
0 goal created.

goal 1/1
(a  c)  (b  c)  a  b  c

%PhoX% intro.
1 goal created.

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

%PhoX% left H.
1 goal created.

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

%PhoX% left H.
2 goals created.

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

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

%PhoX% left H0.
2 goals created.

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

goal 1/3
H := c
a  b  c

%PhoX% trivial.
0 goal created.

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

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

%PhoX% trivial.
0 goal created.

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

%PhoX% left H0.
2 goals created.

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

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

%PhoX% trivial.
0 goal created.

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

%PhoX% intro l.
1 goal created.

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

%PhoX% trivial.
0 goal created.

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

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

>PhoX> theorem numero10 (a  b)c(ac)or(bc).
Here is the goal:
goal 1/1
(a  b)  c  a  c  b  c

%PhoX% intros.
2 goals created.

goal 2/2
a  c  b  c  (a  b)  c

goal 1/2
(a  b)  c  a  c  b  c

%PhoX% intro.
1 goal created.

goal 1/2
H := (a  b)  c
a  c  b  c

%PhoX% left H.
1 goal created.

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

%PhoX% left H.
2 goals created.

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

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

%PhoX% intro r.
1 goal created.

goal 1/3
H0 := c
H := b
b  c

%PhoX% intro.
2 goals created.

goal 2/4
H0 := c
H := b
c

goal 1/4
H0 := c
H := b
b

%PhoX% axiom H.
0 goal created.

goal 3/3
a  c  b  c  (a  b)  c

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

goal 1/3
H0 := c
H := b
c

%PhoX% axiom H0.
0 goal created.

goal 2/2
a  c  b  c  (a  b)  c

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

%PhoX% intro l.
1 goal created.

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

%PhoX% intro.
2 goals created.

goal 2/3
H0 := c
H := a
c

goal 1/3
H0 := c
H := a
a

%PhoX% axiom H.
0 goal created.

goal 2/2
a  c  b  c  (a  b)  c

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

%PhoX% axiom H0.
0 goal created.

goal 1/1
a  c  b  c  (a  b)  c

%PhoX% intro 2.
2 goals created.

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

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

%PhoX% left H.
2 goals created.

goal 2/3
H := a  c
a  b

goal 1/3
H := b  c
a  b

%PhoX% intro r.
1 goal created.

goal 1/3
H := b  c
b

%PhoX% elim H.
0 goal created.

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

goal 1/2
H := a  c
a  b

%PhoX% intro l.
1 goal created.

goal 1/2
H := a  c
a

%PhoX% elim H.
0 goal created.

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

%PhoX% left H.
2 goals created.

goal 2/2
H := a  c
c

goal 1/2
H := b  c
c

%PhoX% elim H.
0 goal created.

goal 1/1
H := a  c
c

%PhoX% elim H.
0 goal created.

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

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

%PhoX% intro.
2 goals created.

goal 2/2
((a  b)  b)  a  b

goal 1/2
a  b  (a  b)  b

%PhoX% intro 2.
1 goal created.

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

%PhoX% elim H.
2 goals created.

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

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

%PhoX% elim H0.
1 goal created.

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

%PhoX% axiom H1.
0 goal created.

goal 2/2
((a  b)  b)  a  b

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

%PhoX% axiom H1.
0 goal created.

goal 1/1
((a  b)  b)  a  b

%PhoX% intro.
1 goal created.

goal 1/1
H := (a  b)  b
a  b

%PhoX% use a   a.
2 goals created.

goal 2/2
H := (a  b)  b
a   a

goal 1/2
H := (a  b)  b
G := a   a
a  b

%PhoX% elim G.
2 goals created.

goal 2/3
H := (a  b)  b
G := a   a
H0 :=  a
a  b

goal 1/3
H := (a  b)  b
G := a   a
H0 := a
a  b

%PhoX% intro l.
1 goal created.

goal 1/3
H := (a  b)  b
G := a   a
H0 := a
a

%PhoX% axiom H0.
0 goal created.

goal 2/2
H := (a  b)  b
a   a

goal 1/2
H := (a  b)  b
G := a   a
H0 :=  a
a  b

%PhoX% intro r.
1 goal created.

goal 1/2
H := (a  b)  b
G := a   a
H0 :=  a
b

%PhoX% elim H.
1 goal created.

goal 1/2
H := (a  b)  b
G := a   a
H0 :=  a
a  b

%PhoX% intro.
1 goal created.

goal 1/2
H := (a  b)  b
G := a   a
H0 :=  a
H1 := a
b

%PhoX% elim H0.
1 goal created.

goal 1/2
H := (a  b)  b
G := a   a
H0 :=  a
H1 := a
a

%PhoX% axiom H1.
0 goal created.

goal 1/1
H := (a  b)  b
a   a

%PhoX% elim  excluded_middle.
0 goal created.

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

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

%PhoX% intros.
2 goals created.

goal 2/2
(a  b  a  b)  a  b

goal 1/2
a  b  a  b  a  b

%PhoX% intros.
1 goal created.

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

%PhoX% left H0.
2 goals created.

goal 2/3
H := a  b
H0 := a
a  b

goal 1/3
H := a  b
H0 := b
a  b

%PhoX% intro.
2 goals created.

goal 2/4
H := a  b
H0 := b
b

goal 1/4
H := a  b
H0 := b
a

%PhoX% elim H.
1 goal created.

goal 1/4
H := a  b
H0 := b
b

%PhoX% axiom H0.
0 goal created.

goal 3/3
(a  b  a  b)  a  b

goal 2/3
H := a  b
H0 := a
a  b

goal 1/3
H := a  b
H0 := b
b

%PhoX% axiom H0.
0 goal created.

goal 2/2
(a  b  a  b)  a  b

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

%PhoX% intro.
2 goals created.

goal 2/3
H := a  b
H0 := a
b

goal 1/3
H := a  b
H0 := a
a

%PhoX% axiom H0.
0 goal created.

goal 2/2
(a  b  a  b)  a  b

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

%PhoX% elim H.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

goal 1/1
(a  b  a  b)  a  b

%PhoX% intros.
1 goal created.

goal 1/1
H := a  b  a  b
a  b

%PhoX% intros.
2 goals created.

goal 2/2
H := a  b  a  b
b  a

goal 1/2
H := a  b  a  b
a  b

%PhoX% intros.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro l.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

goal 1/1
H := a  b  a  b
b  a

%PhoX% intros.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro r.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

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

bye
```