>PhoX> Sort term.
Sort term defined
>PhoX> Cst R : term  prop.
R : term  prop

>PhoX> theorem numero1   xy (R x    R y).
Here is the goal:
goal 1/1
      x y (R x    R y)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y (R x    R y)
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y (R x    R y)
    x y (R x    R y)

%PhoX% intro 4.
1 goal created.

goal 1/1
H :=  x y0 (R x    R y0)
H0 := R ?1
H1 :=  R y
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y0 (R x    R y0)
H0 := R ?1
H1 :=  R y
    x y0 (R x    R y0)

%PhoX% intro 4.
1 goal created.

goal 1/1
H :=  x y1 (R x    R y1)
H0 := R ?1
H1 :=  R y
H2 := R ?2
H3 :=  R y0
    False

%PhoX% elim H1.
1 goal created.

goal 1/1
H :=  x y1 (R x    R y1)
H0 := R ?1
H1 :=  R y
H2 := R ?2
H3 :=  R y0
    R y

%PhoX% axiom H2.
0 goal created.

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

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

>PhoX> theorem numero3      x y (((   R y    R x)     R x )    R y ).
Here is the goal:
goal 1/1
      x y (((  R y    R x)    R x)    R y)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y (((  R y    R x)    R x)    R y)
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y (((  R y    R x)    R x)    R y)
    x y (((  R y    R x)    R x)    R y)

%PhoX% intro 4.
1 goal created.

goal 1/1
H :=  x y0 (((  R y0    R x)    R x)    R y0)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y0 (((  R y0    R x)    R x)    R y0)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
    x y0 (((  R y0    R x)    R x)    R y0)

%PhoX% intro 4.
1 goal created.

goal 1/1
H :=  x y1 (((  R y1    R x)    R x)    R y1)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
H2 := (  R y0    R ?2)    R ?2
H3 :=  R y0
    False

%PhoX% instance ?2 y.
Here is the goal:
goal 1/1
H :=  x y1 (((  R y1    R x)    R x)    R y1)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
H2 := (  R y0    R y)    R y
H3 :=  R y0
    False

%PhoX% elim H2.
2 goals created.

goal 2/2
H :=  x y1 (((  R y1    R x)    R x)    R y1)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
H2 := (  R y0    R y)    R y
H3 :=  R y0
     R y

goal 1/2
H :=  x y1 (((  R y1    R x)    R x)    R y1)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
H2 := (  R y0    R y)    R y
H3 :=  R y0
      R y0    R y

%PhoX% intro 2.
1 goal created.

goal 1/2
H :=  x y1 (((  R y1    R x)    R x)    R y1)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
H2 := (  R y0    R y)    R y
H3 :=  R y0
H4 :=   R y0
    False

%PhoX% elim H4.
1 goal created.

goal 1/2
H :=  x y1 (((  R y1    R x)    R x)    R y1)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
H2 := (  R y0    R y)    R y
H3 :=  R y0
H4 :=   R y0
     R y0

%PhoX% axiom H3.
0 goal created.

goal 1/1
H :=  x y1 (((  R y1    R x)    R x)    R y1)
H0 := (  R y    R ?1)    R ?1
H1 :=  R y
H2 := (  R y0    R y)    R y
H3 :=  R y0
     R y

%PhoX% axiom H1.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero3 =   x y (((  R y    R x)    R x)    R y) : theorem

>PhoX> Sort term.
This symbol already exists (ignored).
Sort term defined
>PhoX> Cst R : term  prop.
This symbol already exists (ignored).
R : term  prop
>PhoX>  Cst S : term  prop.
S : term  prop
>PhoX> (* exercice difficile*)

>PhoX> theorem numero4   xy   (((R y  R x)  R x)  R y).
Here is the goal:
goal 1/1
      x y   (((R y  R x)  R x)  R y)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y   (((R y  R x)  R x)  R y)
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y   (((R y  R x)  R x)  R y)
    x y   (((R y  R x)  R x)  R y)

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y0   (((R y0  R x)  R x)  R y0)
      (((R y  R ?1)  R ?1)  R y)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y0   (((R y0  R x)  R x)  R y0)
H0 :=  (((R y  R ?1)  R ?1)  R y)
    False

%PhoX% elim H0.
1 goal created.

goal 1/1
H :=  x y0   (((R y0  R x)  R x)  R y0)
H0 :=  (((R y  R ?1)  R ?1)  R y)
    ((R y  R ?1)  R ?1)  R y

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y0   (((R y0  R x)  R x)  R y0)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
    R y

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

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y0   (((R y0  R x)  R x)  R y0)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
    x y0   (((R y0  R x)  R x)  R y0)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y0   (((R y0  R x)  R x)  R y0)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
    y0   (((R y0  R ?2)  R ?2)  R y0)

%PhoX% instance ?2 y.
Here is the goal:
goal 1/1
H :=  x y0   (((R y0  R x)  R x)  R y0)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
    y0   (((R y0  R y)  R y)  R y0)

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
    False

%PhoX% elim H2.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
    ((R y0  R y)  R y)  R y0

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
H3 := (R y0  R y)  R y
    R y0

%PhoX% elim H0.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
H3 := (R y0  R y)  R y
    ((R y  R ?1)  R ?1)  R y

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
H3 := (R y0  R y)  R y
    R y

%PhoX% elim H3.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
H3 := (R y0  R y)  R y
    R y0  R y

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
H3 := (R y0  R y)  R y
H5 := R y0
    R y

%PhoX% elim H2.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
H3 := (R y0  R y)  R y
H5 := R y0
    ((R y0  R y)  R y)  R y0

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y1   (((R y1  R x)  R x)  R y1)
H0 :=  (((R y  R ?1)  R ?1)  R y)
H1 := (R y  R ?1)  R ?1
H2 :=  (((R y0  R y)  R y)  R y0)
H3 := (R y0  R y)  R y
H5 := R y0
    R y0

%PhoX% axiom H5.
0 goal created.

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

>PhoX> (* comme le précédent mais un peu plus dur !*)

>PhoX> theorem numero6    xy   ((S y  R x)  (S x  R y)).
Here is the goal:
goal 1/1
      x y   ((S y  R x)  S x  R y)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y   ((S y  R x)  S x  R y)
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y   ((S y  R x)  S x  R y)
    x y   ((S y  R x)  S x  R y)

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y0   ((S y0  R x)  S x  R y0)
      ((S y  R ?1)  S ?1  R y)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y0   ((S y0  R x)  S x  R y0)
H0 :=  ((S y  R ?1)  S ?1  R y)
    False

%PhoX% elim H0.
1 goal created.

goal 1/1
H :=  x y0   ((S y0  R x)  S x  R y0)
H0 :=  ((S y  R ?1)  S ?1  R y)
    (S y  R ?1)  S ?1  R y

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y0   ((S y0  R x)  S x  R y0)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
    R y

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y0   ((S y0  R x)  S x  R y0)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
    x y0   ((S y0  R x)  S x  R y0)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y0   ((S y0  R x)  S x  R y0)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
    y0   ((S y0  R ?2)  S ?2  R y0)

%PhoX% instance ?2 y.
Here is the goal:
goal 1/1
H :=  x y0   ((S y0  R x)  S x  R y0)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
    y0   ((S y0  R y)  S y  R y0)

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y1   ((S y1  R x)  S x  R y1)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
    False

%PhoX% elim H3.
1 goal created.

goal 1/1
H :=  x y1   ((S y1  R x)  S x  R y1)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
    (S y0  R y)  S y  R y0

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y1   ((S y1  R x)  S x  R y1)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
    R y0

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y1   ((S y1  R x)  S x  R y1)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
    x y1   ((S y1  R x)  S x  R y1)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y1   ((S y1  R x)  S x  R y1)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
    y1   ((S y1  R ?3)  S ?3  R y1)

%PhoX% instance ?3 y0.
Here is the goal:
goal 1/1
H :=  x y1   ((S y1  R x)  S x  R y1)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
    y1   ((S y1  R y0)  S y0  R y1)

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y2   ((S y2  R x)  S x  R y2)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
H6 :=  ((S y1  R y0)  S y0  R y1)
    False

%PhoX% elim H6.
1 goal created.

goal 1/1
H :=  x y2   ((S y2  R x)  S x  R y2)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
H6 :=  ((S y1  R y0)  S y0  R y1)
    (S y1  R y0)  S y0  R y1

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y2   ((S y2  R x)  S x  R y2)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
H6 :=  ((S y1  R y0)  S y0  R y1)
H7 := S y1  R y0
H8 := S y0
    R y1

%PhoX% elim H3.
1 goal created.

goal 1/1
H :=  x y2   ((S y2  R x)  S x  R y2)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
H6 :=  ((S y1  R y0)  S y0  R y1)
H7 := S y1  R y0
H8 := S y0
    (S y0  R y)  S y  R y0

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y2   ((S y2  R x)  S x  R y2)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
H6 :=  ((S y1  R y0)  S y0  R y1)
H7 := S y1  R y0
H8 := S y0
    R y0

%PhoX% elim H0.
1 goal created.

goal 1/1
H :=  x y2   ((S y2  R x)  S x  R y2)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
H6 :=  ((S y1  R y0)  S y0  R y1)
H7 := S y1  R y0
H8 := S y0
    (S y  R ?1)  S ?1  R y

%PhoX% intro 2.
1 goal created.

goal 1/1
H :=  x y2   ((S y2  R x)  S x  R y2)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
H6 :=  ((S y1  R y0)  S y0  R y1)
H7 := S y1  R y0
H8 := S y0
    R y

%PhoX% elim H4.
1 goal created.

goal 1/1
H :=  x y2   ((S y2  R x)  S x  R y2)
H0 :=  ((S y  R ?1)  S ?1  R y)
H1 := S y  R ?1
H2 := S ?1
H3 :=  ((S y0  R y)  S y  R y0)
H4 := S y0  R y
H5 := S y
H6 :=  ((S y1  R y0)  S y0  R y1)
H7 := S y1  R y0
H8 := S y0
    S y0

%PhoX% axiom H8.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero6 =   x y   ((S y  R x)  S x  R y) : theorem

>PhoX> Cst f : term  term.
f : term  term

>PhoX> theorem numero7    xy (((R (f x)    R (f y))  R x)    R y).
Here is the goal:
goal 1/1
      x y (((R (f x)    R (f y))  R x)    R y)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y (((R (f x)    R (f y))  R x)    R y)
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y (((R (f x)    R (f y))  R x)    R y)
    x y (((R (f x)    R (f y))  R x)    R y)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y (((R (f x)    R (f y))  R x)    R y)
    y (((R (f ?1)    R (f y))  R ?1)    R y)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y0 (((R (f x)    R (f y0))  R x)    R y0)
H0 := (R (f ?1)    R (f y))  R ?1
      R y

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y0 (((R (f x)    R (f y0))  R x)    R y0)
H0 := (R (f ?1)    R (f y))  R ?1
H1 :=  R y
    False

%PhoX% rmh H0.
1 goal created.

goal 1/1
H :=  x y0 (((R (f x)    R (f y0))  R x)    R y0)
H1 :=  R y
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y0 (((R (f x)    R (f y0))  R x)    R y0)
H1 :=  R y
    x y0 (((R (f x)    R (f y0))  R x)    R y0)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y0 (((R (f x)    R (f y0))  R x)    R y0)
H1 :=  R y
    y0 (((R (f ?2)    R (f y0))  R ?2)    R y0)

%PhoX% instance ?2 y.
Here is the goal:
goal 1/1
H :=  x y0 (((R (f x)    R (f y0))  R x)    R y0)
H1 :=  R y
    y0 (((R (f y)    R (f y0))  R y)    R y0)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
      R y0

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
    False

%PhoX% elim H1.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
    R y

%PhoX% elim H0.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
    R (f y)    R (f y0)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
      R (f y0)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
    x y1 (((R (f x)    R (f y1))  R x)    R y1)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
    y1 (((R (f ?3)    R (f y1))  R ?3)    R y1)

%PhoX% instance ?3 y0.
Here is the goal:
goal 1/1
H :=  x y1 (((R (f x)    R (f y1))  R x)    R y1)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
    y1 (((R (f y0)    R (f y1))  R y0)    R y1)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y2 (((R (f x)    R (f y2))  R x)    R y2)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
H5 := (R (f y0)    R (f y1))  R y0
      R y1

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y2 (((R (f x)    R (f y2))  R x)    R y2)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
H5 := (R (f y0)    R (f y1))  R y0
H6 :=  R y1
    False

%PhoX% elim H2.
1 goal created.

goal 1/1
H :=  x y2 (((R (f x)    R (f y2))  R x)    R y2)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
H5 := (R (f y0)    R (f y1))  R y0
H6 :=  R y1
    R y0

%PhoX% elim H5.
1 goal created.

goal 1/1
H :=  x y2 (((R (f x)    R (f y2))  R x)    R y2)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
H5 := (R (f y0)    R (f y1))  R y0
H6 :=  R y1
    R (f y0)    R (f y1)

%PhoX% intros.
1 goal created.

goal 1/1
H :=  x y2 (((R (f x)    R (f y2))  R x)    R y2)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
H5 := (R (f y0)    R (f y1))  R y0
H6 :=  R y1
H7 := R (f y0)
      R (f y1)

%PhoX% elim H4.
1 goal created.

goal 1/1
H :=  x y2 (((R (f x)    R (f y2))  R x)    R y2)
H1 :=  R y
H0 := (R (f y)    R (f y0))  R y
H2 :=  R y0
H3 := R (f y)
H4 :=  R (f y0)
H5 := (R (f y0)    R (f y1))  R y0
H6 :=  R y1
H7 := R (f y0)
    R (f y0)

%PhoX% axiom H7.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero7 =   x y (((R (f x)    R (f y))  R x)    R y) : theorem

bye