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

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

%PhoX% use x R x   x R x.
2 goals created.

goal 2/2
    x R x   x R x

goal 1/2
G := x R x   x R x
    x y:R  R x

%PhoX% left G.
2 goals created.

goal 2/3
H := x R x
    x y:R  R x

goal 1/3
H :=  x R x
    x y:R  R x

%PhoX% rewrite_hyp H exists.demorgan.
1 goal created.

goal 1/3
H := x  R x
    x y:R  R x

%PhoX% intro 3.
1 goal created.

goal 1/3
H := x  R x
H0 := R y
    R ?1

%PhoX% elim False.
1 goal created.

goal 1/3
H := x  R x
H0 := R y
    False

%PhoX% apply -1 (y) H.
1 goal created.

goal 1/3
H := x  R x
H0 := R y
G :=  R y
    False

%PhoX% elim G.
1 goal created.

goal 1/3
H := x  R x
H0 := R y
G :=  R y
    R y

%PhoX% axiom H0.
0 goal created.

goal 2/2
    x R x   x R x

goal 1/2
H := x R x
    x y:R  R x

%PhoX% elim H.
1 goal created.

goal 1/2
H := x0 R x0
H0 := R x
    x0 y:R  R x0

%PhoX% intro.
1 goal created.

goal 1/2
H := x0 R x0
H0 := R x
    y:R  R ?2

%PhoX% instance ?2 x.
Here are the goals:
goal 2/2
    x R x   x R x

goal 1/2
H := x0 R x0
H0 := R x
    y:R  R x

%PhoX% intro 2.
1 goal created.

goal 1/2
H := x0 R x0
H0 := R x
H1 := R y
    R x

%PhoX% axiom H0.
0 goal created.

goal 1/1
    x R x   x R x

%PhoX% elim excluded_middle.
0 goal created.

%PhoX% save numero2.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero2 = x y:R  R x : theorem


>PhoX> theorem numero3 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% use x R x   x R x.
2 goals created.

goal 2/2
    x R x   x R x

goal 1/2
G := x R x   x R x
    x y (((R y  R x)  R x)  R y)

%PhoX% elim G.
2 goals created.

goal 2/3
G := x R x   x R x
H :=  x R x
    x y (((R y  R x)  R x)  R y)

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

%PhoX% intro 3.
1 goal created.

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

%PhoX% elim H.
0 goal created.

goal 2/2
    x R x   x R x

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

%PhoX% rewrite_hyp H forall.demorgan.
1 goal created.

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

%PhoX% elim H.
1 goal created.

goal 1/2
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
    x0 y (((R y  R x0)  R x0)  R y)

%PhoX% intro 3.
1 goal created.

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

%PhoX% instance ?2 x.
Here are the goals:
goal 2/2
    x R x   x R x

goal 1/2
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
    R y

%PhoX% use R y   R y.
2 goals created.

goal 2/3
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
    R y   R y

goal 1/3
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
G0 := R y   R y
    R y

%PhoX% elim G0.
2 goals created.

goal 2/4
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
G0 := R y   R y
H2 :=  R y
    R y

goal 1/4
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
G0 := R y   R y
H2 := R y
    R y

%PhoX% axiom H2.
0 goal created.

goal 3/3
    x R x   x R x

goal 2/3
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
    R y   R y

goal 1/3
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
G0 := R y   R y
H2 :=  R y
    R y

%PhoX% elim H0.
1 goal created.

goal 1/3
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
G0 := R y   R y
H2 :=  R y
    R x

%PhoX% elim H1.
1 goal created.

goal 1/3
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
G0 := R y   R y
H2 :=  R y
    R y  R x

%PhoX% intro.
1 goal created.

goal 1/3
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
G0 := R y   R y
H2 :=  R y
H3 := R y
    R x

%PhoX% elim H2.
1 goal created.

goal 1/3
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
G0 := R y   R y
H2 :=  R y
H3 := R y
    R y

%PhoX% axiom H3.
0 goal created.

goal 2/2
    x R x   x R x

goal 1/2
G := x0 R x0   x0 R x0
H := x0  R x0
H0 :=  R x
H1 := (R y  R x)  R x
    R y   R y

%PhoX% elim excluded_middle.
0 goal created.

goal 1/1
    x R x   x R x

%PhoX% elim excluded_middle.
0 goal created.

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

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

>PhoX> theorem numero5 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% by_absurd.
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% intro 3.
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% rmh H0.
1 goal created.

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

%PhoX% by_absurd.
1 goal created.

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

%PhoX% elim H.
1 goal created.

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

%PhoX% intro 3.
1 goal created.

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

%PhoX% by_absurd.
1 goal created.

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

%PhoX% elim H0.
1 goal created.

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

%PhoX% elim H1.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% by_absurd.
1 goal created.

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

%PhoX% elim H.
1 goal created.

goal 1/1
H :=  x y1 (((R (f x)  R (f y1))  R x)  R y1)
H0 :=  R y
H1 := (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% intro 3.
1 goal created.

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

%PhoX% elim H2.
1 goal created.

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

%PhoX% elim H5.
1 goal created.

goal 1/1
H :=  x y2 (((R (f x)  R (f y2))  R x)  R y2)
H0 :=  R y
H1 := (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 (f y0)  R (f y1)

%PhoX% intro.
1 goal created.

goal 1/1
H :=  x y2 (((R (f x)  R (f y2))  R x)  R y2)
H0 :=  R y
H1 := (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 (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)
H0 :=  R y
H1 := (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 (f y0)
    R (f y0)

%PhoX% axiom H6.
0 goal created.

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

bye