>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