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

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

%PhoX% intro 3.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H0.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H2.
1 goal created.

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

%PhoX% elim H3.
1 goal created.

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

%PhoX% axiom H1.
0 goal created.

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

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro 3.
1 goal created.

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

%PhoX% elim H1.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro 3.
1 goal created.

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

%PhoX% elim H2.
1 goal created.

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

%PhoX% elim H0.
1 goal created.

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

%PhoX% axiom H3.
0 goal created.

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

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro 2.
1 goal created.

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

%PhoX% elim H0.
2 goals created.

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

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro 2.
1 goal created.

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

%PhoX% axiom H2.
0 goal created.

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

%PhoX% axiom H1.
0 goal created.

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

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H0.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% (* la commande suivante correspond à la règle d'absurdité intuitionniste*)

%PhoX% elim False.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% axiom H1.
0 goal created.

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

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% intro l.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% (* la commande suivante correspond à la règle d'absurdité intuitionniste*)

%PhoX% elim H.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% intro r.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H0.
1 goal created.

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

%PhoX% intro.
2 goals created.

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

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

%PhoX% axiom H1.
0 goal created.

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

%PhoX% axiom H3.
0 goal created.

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

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

%PhoX% intros.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intros.
1 goal created.

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

%PhoX% intro l.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H0.
3 goals created.

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

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

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

%PhoX% axiom H1.
0 goal created.

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

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

%PhoX% axiom H2.
0 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intros.
1 goal created.

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

%PhoX% intro r.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% axiom H2.
0 goal created.

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

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

%PhoX% intros.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intros.
1 goal created.

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

%PhoX% intro l.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H0.
3 goals created.

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

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

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

%PhoX% axiom H1.
0 goal created.

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

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

%PhoX% axiom H2.
0 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intros.
1 goal created.

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

%PhoX% intro r.
1 goal created.

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

%PhoX% axiom H2.
0 goal created.

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

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

%PhoX% intros.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intros.
1 goal created.

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

%PhoX% intro r.
1 goal created.

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

%PhoX% elim H0.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intros.
1 goal created.

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

%PhoX% intro l.
1 goal created.

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

%PhoX% axiom H1.
0 goal created.

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

bye
```