>PhoX> Sort term.
Sort term defined
>PhoX> Cst R : term  term  prop.
R : term  term  prop
>PhoX> Cst f : term  term  term.
f : term  term  term
>PhoX> goal
>PhoX>   x,y,z (R x y  R y z  R x z)  
>PhoX>   x,y,z (R(f (f x y) z) (f x (f y z)))  
>PhoX>   x,y,z (R x y  R (f x z) (f y z)) 
>PhoX>   x,y (R x y  R y x)  
>PhoX> x,y,u,v (R (f x (f (f y u) v)) (f (f (f x y) u) v)).
Here is the goal:
goal 1/1
    x,y,z (R x y  R y z  R x z) 
        x,y,z R (f (f x y) z) (f x (f y z)) 
        x,y,z (R x y  R (f x z) (f y z))  x,y (R x y  R y x) 
        x,y,u,v R (f x (f (f y u) v)) (f (f (f x y) u) v)

%PhoX% intro A1 A2 A3 A4.
1 goal created.

goal 1/1
A1 := x,y,z (R x y  R y z  R x z)
A2 := x,y,z R (f (f x y) z) (f x (f y z))
A3 := x,y,z (R x y  R (f x z) (f y z))
A4 := x,y (R x y  R y x)
    x,y,u,v R (f x (f (f y u) v)) (f (f (f x y) u) v)

%PhoX% intros.
1 goal created.

goal 1/1
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R (f x (f (f y u) v)) (f (f (f x y) u) v)

%PhoX% elim A4.
1 goal created.

goal 1/1
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R (f (f (f x y) u) v) (f x (f (f y u) v))

%PhoX% elim A1.
1 goal created.

goal 1/1
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R (f (f (f x y) u) v) ?1  R ?1 (f x (f (f y u) v))

%PhoX% intro.
2 goals created.

goal 2/2
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R ?1 (f x (f (f y u) v))

goal 1/2
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R (f (f (f x y) u) v) ?1

%PhoX% next.
Here are the goals:
goal 2/2
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R (f (f (f x y) u) v) ?1

goal 1/2
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R ?1 (f x (f (f y u) v))

%PhoX% elim A2.
0 goal created.

goal 1/1
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R (f (f (f x y) u) v) (f (f x (f y u)) v)

%PhoX% elim A3.
1 goal created.

goal 1/1
A1 := x0,y0,z (R x0 y0  R y0 z  R x0 z)
A2 := x0,y0,z R (f (f x0 y0) z) (f x0 (f y0 z))
A3 := x0,y0,z (R x0 y0  R (f x0 z) (f y0 z))
A4 := x0,y0 (R x0 y0  R y0 x0)
    R (f (f x y) u) (f x (f y u))

%PhoX% elim A2.
0 goal created.

%PhoX% save th.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
th =
   x,y,z (R x y  R y z  R x z)  x,y,z R (f (f x y) z) (f x (f y z)) 
     x,y,z (R x y  R (f x z) (f y z))  x,y (R x y  R y x) 
     x,y,u,v R (f x (f (f y u) v)) (f (f (f x y) u) v) : 
theorem

bye