>PhoX> Sort term.
Sort term defined
>PhoX> Cst P : term  prop.
P : term  prop
>PhoX> Cst R : term  prop.
R : term  prop
>PhoX> Cst T : term  term  prop.
T : term  term  prop
>PhoX> Cst S : term  prop.
S : term  prop
>PhoX> goal xy(P x (R y  T x y)) x,y( P x   S y   T x y)  x( R x   S x).
Here is the goal:
goal 1/1
    x y (P x  (R y  T x y))  x,y ( P x   S y   T x y) 
        x ( R x   S x)

%PhoX% intro 3.
1 goal created.

goal 1/1
H := x0 y (P x0  (R y  T x0 y))
H0 := x0,y ( P x0   S y   T x0 y)
     R x   S x

%PhoX% by_absurd.
1 goal created.

goal 1/1
H := x0 y (P x0  (R y  T x0 y))
H0 := x0,y ( P x0   S y   T x0 y)
H1 :=  ( R x   S x)
     R x   S x

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

goal 1/1
H := x0 y (P x0  (R y  T x0 y))
H0 := x0,y ( P x0   S y   T x0 y)
H1 :=   R x    S x
     R x   S x

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

goal 1/1
H := x0 y (P x0  (R y  T x0 y))
H0 := x0,y ( P x0   S y   T x0 y)
H1 := R x  S x
     R x   S x

%PhoX% elim False.
1 goal created.

goal 1/1
H := x0 y (P x0  (R y  T x0 y))
H0 := x0,y ( P x0   S y   T x0 y)
H1 := R x  S x
    False

%PhoX% left H1.
1 goal created.

goal 1/1
H := x0 y (P x0  (R y  T x0 y))
H0 := x0,y ( P x0   S y   T x0 y)
H1 := R x
H2 := S x
    False

%PhoX% elim H.
1 goal created.

goal 1/1
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
    False

%PhoX% apply -1 (x) H3.
1 goal created.

goal 1/1
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
G := P x0  (R x  T x0 x)
    False

%PhoX% left G.
1 goal created.

goal 1/1
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
    False

%PhoX% apply -1 (x0) -2 (x) H0.
1 goal created.

goal 1/1
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
    False

%PhoX% use T x0 x.
2 goals created.

goal 2/2
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
    T x0 x

goal 1/2
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
    False

%PhoX% elim G.
2 goals created.

goal 2/3
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  T x0 x
    False

goal 1/3
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  P x0   S x
    False

%PhoX% elim H6.
2 goals created.

goal 2/4
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  P x0   S x
H7 :=  S x
    False

goal 1/4
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  P x0   S x
H7 :=  P x0
    False

%PhoX% elim H7.
1 goal created.

goal 1/4
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  P x0   S x
H7 :=  P x0
    P x0

%PhoX% axiom H4.
0 goal created.

goal 3/3
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
    T x0 x

goal 2/3
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  T x0 x
    False

goal 1/3
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  P x0   S x
H7 :=  S x
    False

%PhoX% elim H7.
1 goal created.

goal 1/3
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  P x0   S x
H7 :=  S x
    S x

%PhoX% axiom H2.
0 goal created.

goal 2/2
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
    T x0 x

goal 1/2
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  T x0 x
    False

%PhoX% elim H6.
1 goal created.

goal 1/2
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
G0 := T x0 x
H6 :=  T x0 x
    T x0 x

%PhoX% axiom G0.
0 goal created.

goal 1/1
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
    T x0 x

%PhoX% elim H5.
1 goal created.

goal 1/1
H := x1 y (P x1  (R y  T x1 y))
H0 := x1,y ( P x1   S y   T x1 y)
H1 := R x
H2 := S x
H3 := y (P x0  (R y  T x0 y))
H4 := P x0
H5 := R x  T x0 x
G :=  P x0   S x   T x0 x
    R x

%PhoX% axiom H1.
0 goal created.

%PhoX% save th.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
th =
   x y (P x  (R y  T x y))  x,y ( P x   S y   T x y) 
     x ( R x   S x) : theorem

bye