>PhoX> Sort term.
Sort term defined
>PhoX> Cst f : term term.
f : term  term
>PhoX> Cst g : term term.
g : term  term
>PhoX> def surj f = y x f x = y.
surj = \f0 y x f0 x = y : ('b  'a)  prop
>PhoX> def inj f =  x,y ((f x) = (f y)   x = y).
inj =
                                                 \f0
                                                  x,y (f0 x = f0 y  x = y)
                                               : ('b  'a)  prop
>PhoX> def bij f = inj f  surj f.
bij = \f0 (inj f0  surj f0) : ('b  'a)  prop
>PhoX> def I = x,y(f (g x)=f (g y)  x=y).
I = x,y (f (g x) = f (g y)  x = y)
                                        : prop
>PhoX> def S = y x f (g x) =y.
S = y x f (g x) = y : prop

>PhoX> theorem numero3 inj f   inj g  I.
Here is the goal:
goal 1/1
    inj f  inj g  I

%PhoX% intro 4.
1 goal created.

goal 1/1
H := inj f  inj g
H0 := f (g x) = f (g y)
    x = y

%PhoX% left H.
1 goal created.

goal 1/1
H0 := f (g x) = f (g y)
H := inj f
H1 := inj g
    x = y

%PhoX% apply H with H0.
1 goal created.

goal 1/1
H0 := f (g x) = f (g y)
H := inj f
H1 := inj g
G := g x = g y
    x = y

%PhoX% apply H1 with G.
1 goal created.

goal 1/1
H0 := f (g x) = f (g y)
H := inj f
H1 := inj g
G := g x = g y
G0 := x = y
    x = y

%PhoX% axiom G0.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero3 = inj f  inj g  I : theorem


>PhoX> theorem numero4 surj f   surj g  S.
Here is the goal:
goal 1/1
    surj f  surj g  S

%PhoX% intro 2.
1 goal created.

goal 1/1
H := surj f  surj g
    x f (g x) = y

%PhoX% left H.
1 goal created.

goal 1/1
H := surj f
H0 := surj g
    x f (g x) = y

%PhoX% elim H.
1 goal created.

goal 1/1
H := surj f
H0 := surj g
H1 := f x = ?1
    x0 f (g x0) = y

%PhoX% elim H0.
1 goal created.

goal 1/1
H := surj f
H0 := surj g
H1 := f x = ?1
H2 := g x0 = ?2
    x1 f (g x1) = y

%PhoX% instance ?1 y.
Here is the goal:
goal 1/1
H := surj f
H0 := surj g
H1 := f x = y
H2 := g x0 = ?2
    x1 f (g x1) = y

%PhoX% instance ?2 x.
Here is the goal:
goal 1/1
H := surj f
H0 := surj g
H1 := f x = y
H2 := g x0 = x
    x1 f (g x1) = y

%PhoX% intro.
1 goal created.

goal 1/1
H := surj f
H0 := surj g
H1 := f x = y
H2 := g x0 = x
    f (g ?3) = y

%PhoX% instance ?3 x0.
Here is the goal:
goal 1/1
H := surj f
H0 := surj g
H1 := f x = y
H2 := g x0 = x
    f (g x0) = y

%PhoX% trivial.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero4 = surj f  surj g  S : theorem


>PhoX> theorem numero5 bij f  bij g  I  S.
Here is the goal:
goal 1/1
    bij f  bij g  I  S

%PhoX% intro 3.
2 goals created.

goal 2/2
H := bij f
H0 := bij g
    S

goal 1/2
H := bij f
H0 := bij g
    I

%PhoX% intro 3.
1 goal created.

goal 1/2
H := bij f
H0 := bij g
H1 := f (g x) = f (g y)
    x = y

%PhoX% use g x = g y.
2 goals created.

goal 2/3
H := bij f
H0 := bij g
H1 := f (g x) = f (g y)
    g x = g y

goal 1/3
H := bij f
H0 := bij g
H1 := f (g x) = f (g y)
G := g x = g y
    x = y

%PhoX% elim H0.
1 goal created.

goal 1/3
H := bij f
H0 := bij g
H1 := f (g x) = f (g y)
G := g x = g y
    g x = g y

%PhoX% axiom G.
0 goal created.

goal 2/2
H := bij f
H0 := bij g
    S

goal 1/2
H := bij f
H0 := bij g
H1 := f (g x) = f (g y)
    g x = g y

%PhoX% elim H.
1 goal created.

goal 1/2
H := bij f
H0 := bij g
H1 := f (g x) = f (g y)
    f (g x) = f (g y)

%PhoX% axiom H1.
0 goal created.

goal 1/1
H := bij f
H0 := bij g
    S

%PhoX% intro.
1 goal created.

goal 1/1
H := bij f
H0 := bij g
    x f (g x) = y

%PhoX% use z f z = y.
2 goals created.

goal 2/2
H := bij f
H0 := bij g
    z f z = y

goal 1/2
H := bij f
H0 := bij g
G := z f z = y
    x f (g x) = y

%PhoX% elim G.
1 goal created.

goal 1/2
H := bij f
H0 := bij g
G := z0 f z0 = y
H1 := f z = y
    x f (g x) = y

%PhoX% use u g u =z.
2 goals created.

goal 2/3
H := bij f
H0 := bij g
G := z0 f z0 = y
H1 := f z = y
    u g u = z

goal 1/3
H := bij f
H0 := bij g
G := z0 f z0 = y
H1 := f z = y
G0 := u g u = z
    x f (g x) = y

%PhoX% elim G0.
1 goal created.

goal 1/3
H := bij f
H0 := bij g
G := z0 f z0 = y
H1 := f z = y
G0 := u0 g u0 = z
H2 := g u = z
    x f (g x) = y

%PhoX% intro.
1 goal created.

goal 1/3
H := bij f
H0 := bij g
G := z0 f z0 = y
H1 := f z = y
G0 := u0 g u0 = z
H2 := g u = z
    f (g ?1) = y

%PhoX% instance ?1 u.
Here are the goals:
goal 3/3
H := bij f
H0 := bij g
    z f z = y

goal 2/3
H := bij f
H0 := bij g
G := z0 f z0 = y
H1 := f z = y
    u g u = z

goal 1/3
H := bij f
H0 := bij g
G := z0 f z0 = y
H1 := f z = y
G0 := u0 g u0 = z
H2 := g u = z
    f (g u) = y

%PhoX% intro.
0 goal created.

goal 2/2
H := bij f
H0 := bij g
    z f z = y

goal 1/2
H := bij f
H0 := bij g
G := z0 f z0 = y
H1 := f z = y
    u g u = z

%PhoX% elim H0.
0 goal created.

goal 1/1
H := bij f
H0 := bij g
    z f z = y

%PhoX% elim H.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero5 = bij f  bij g  I  S : theorem


>PhoX> theorem numero6  I  inj g.
Here is the goal:
goal 1/1
    I  inj g

%PhoX% intro 4.
1 goal created.

goal 1/1
H := I
H0 := g x = g y
    x = y

%PhoX% use f (g x)=f (g y).
2 goals created.

goal 2/2
H := I
H0 := g x = g y
    f (g x) = f (g y)

goal 1/2
H := I
H0 := g x = g y
G := f (g x) = f (g y)
    x = y

%PhoX% elim H.
1 goal created.

goal 1/2
H := I
H0 := g x = g y
G := f (g x) = f (g y)
    f (g x) = f (g y)

%PhoX% axiom G.
0 goal created.

goal 1/1
H := I
H0 := g x = g y
    f (g x) = f (g y)

%PhoX% intro.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero6 = I  inj g : theorem


>PhoX> theorem numero7 S  surj f.
Here is the goal:
goal 1/1
    S  surj f

%PhoX% intros.
1 goal created.

goal 1/1
H := S
    surj f

%PhoX% intros.
1 goal created.

goal 1/1
H := S
    x f x = y

%PhoX% unfold_hyp H S.
1 goal created.

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

%PhoX% elim H with y.
1 goal created.

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

%PhoX% intro.
1 goal created.

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

%PhoX% axiom H0.
0 goal created.

%PhoX% save.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
numero7 = S  surj f : theorem

bye