>PhoX> Sort term.
Sort term defined
>PhoX> Cst f : term  term.
f : term  term
>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 surj f = y x (f x = y).
surj = \f0 y x f0 x = y
                                 : ('b  'a)  prop
>PhoX> Cst a : term.
a : term
>PhoX> Cst b : term.
b : term
>PhoX> def au_plus_deux = x (x = a  x = b).
au_plus_deux =
                                         x (x = a  x = b) :
                                         prop
>PhoX> goal au_plus_deux  (inj f  surj f).
Here is the goal:
goal 1/1
    au_plus_deux  inj f  surj f

%PhoX% intros.
1 goal created.

goal 1/1
H := au_plus_deux
    inj f  surj f

%PhoX% intros.
2 goals created.

goal 2/2
H := au_plus_deux
    surj f  inj f

goal 1/2
H := au_plus_deux
    inj f  surj f

%PhoX% intros.
1 goal created.

goal 1/2
H := au_plus_deux
H0 := inj f
    surj f

%PhoX% intros.
1 goal created.

goal 1/2
H := au_plus_deux
H0 := inj f
    x f x = y

%PhoX% elim H with y.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := inj f
H1 := y = b
    x f x = y

goal 1/3
H := au_plus_deux
H0 := inj f
H1 := y = a
    x f x = y

%PhoX% elim H with f a.
2 goals created.

goal 2/4
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
    x f x = y

goal 1/4
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = a
    x f x = y

%PhoX% intro.
1 goal created.

goal 1/4
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = a
    f ?1 = y

%PhoX% axiom H2.
0 goal created.

goal 3/3
H := au_plus_deux
    surj f  inj f

goal 2/3
H := au_plus_deux
H0 := inj f
H1 := y = b
    x f x = y

goal 1/3
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
    x f x = y

%PhoX% elim H with f b.
2 goals created.

goal 2/4
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
H3 := f b = b
    x f x = y

goal 1/4
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
H3 := f b = a
    x f x = y

%PhoX% intro.
1 goal created.

goal 1/4
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
H3 := f b = a
    f ?2 = y

%PhoX% axiom H3.
0 goal created.

goal 3/3
H := au_plus_deux
    surj f  inj f

goal 2/3
H := au_plus_deux
H0 := inj f
H1 := y = b
    x f x = y

goal 1/3
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
H3 := f b = b
    x f x = y

%PhoX% apply 3 H0 with a and b.
2 goals created.

goal 2/4
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
H3 := f b = b
G := a = b
    x f x = y

goal 1/4
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
H3 := f b = b
    f a = f b

%PhoX% intro.
0 goal created.

goal 3/3
H := au_plus_deux
    surj f  inj f

goal 2/3
H := au_plus_deux
H0 := inj f
H1 := y = b
    x f x = y

goal 1/3
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
H3 := f b = b
G := a = b
    x f x = y

%PhoX% intro.
1 goal created.

goal 1/3
H := au_plus_deux
H0 := inj f
H1 := y = a
H2 := f a = b
H3 := f b = b
G := a = b
    f ?3 = y

%PhoX% axiom H2.
0 goal created.

goal 2/2
H := au_plus_deux
    surj f  inj f

goal 1/2
H := au_plus_deux
H0 := inj f
H1 := y = b
    x f x = y

%PhoX% elim H with f a.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = b
    x f x = y

goal 1/3
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
    x f x = y

%PhoX% elim H with f b.
2 goals created.

goal 2/4
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = b
    x f x = y

goal 1/4
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = a
    x f x = y

%PhoX% apply 3 H0 with a and b.
2 goals created.

goal 2/5
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = a
G := a = b
    x f x = y

goal 1/5
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = a
    f a = f b

%PhoX% intro.
0 goal created.

goal 4/4
H := au_plus_deux
    surj f  inj f

goal 3/4
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = b
    x f x = y

goal 2/4
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = b
    x f x = y

goal 1/4
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = a
G := a = b
    x f x = y

%PhoX% intro.
1 goal created.

goal 1/4
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = a
G := a = b
    f ?4 = y

%PhoX% axiom H2.
0 goal created.

goal 3/3
H := au_plus_deux
    surj f  inj f

goal 2/3
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = b
    x f x = y

goal 1/3
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = b
    x f x = y

%PhoX% intro.
1 goal created.

goal 1/3
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = a
H3 := f b = b
    f ?5 = y

%PhoX% axiom H3.
0 goal created.

goal 2/2
H := au_plus_deux
    surj f  inj f

goal 1/2
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = b
    x f x = y

%PhoX% intro.
1 goal created.

goal 1/2
H := au_plus_deux
H0 := inj f
H1 := y = b
H2 := f a = b
    f ?6 = y

%PhoX% axiom H2.
0 goal created.

goal 1/1
H := au_plus_deux
    surj f  inj f

%PhoX% intros.
1 goal created.

goal 1/1
H := au_plus_deux
H0 := surj f
    inj f

%PhoX% intros.
1 goal created.

goal 1/1
H := au_plus_deux
H0 := surj f
H1 := f x = f y
    x = y

%PhoX% elim H with x.
2 goals created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
    x = y

%PhoX% elim H with y.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = a
    x = y

%PhoX% intro.
0 goal created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
    x = y

%PhoX% elim H with f a.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = a
    x = y

%PhoX% prove f b = a.
2 goals created.

goal 2/4
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = a
G := f b = a
    x = y

goal 1/4
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = a
    f b = a

%PhoX% intro.
0 goal created.

goal 3/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
    x = y

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = a
G := f b = a
    x = y

%PhoX% elim H0 with b.
1 goal created.

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = a
G := f b = a
H5 := f x0 = b
    x = y

%PhoX% elim H with x0.
2 goals created.

goal 2/4
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = a
G := f b = a
H5 := f x0 = b
H6 := x0 = b
    x = y

goal 1/4
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = a
G := f b = a
H5 := f x0 = b
H6 := x0 = a
    x = y

%PhoX% intro.
0 goal created.

goal 3/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
    x = y

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = a
G := f b = a
H5 := f x0 = b
H6 := x0 = b
    x = y

%PhoX% intro.
0 goal created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
    x = y

%PhoX% prove f b = b.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
G := f b = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
    f b = b

%PhoX% intro.
0 goal created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
G := f b = b
    x = y

%PhoX% elim H0 with a.
1 goal created.

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
G := f b = b
H5 := f x0 = a
    x = y

%PhoX% elim H with x0.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
G := f b = b
H5 := f x0 = a
H6 := x0 = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
G := f b = b
H5 := f x0 = a
H6 := x0 = a
    x = y

%PhoX% intro.
0 goal created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = a
H3 := y = b
H4 := f a = b
G := f b = b
H5 := f x0 = a
H6 := x0 = b
    x = y

%PhoX% intro.
0 goal created.

goal 1/1
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
    x = y

%PhoX% elim H with y.
2 goals created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
    x = y

%PhoX% elim H with f a.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = a
    x = y

%PhoX% prove f b = a.
2 goals created.

goal 2/4
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = a
G := f b = a
    x = y

goal 1/4
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = a
    f b = a

%PhoX% intro.
0 goal created.

goal 3/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = b
    x = y

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = a
G := f b = a
    x = y

%PhoX% elim H0 with b.
1 goal created.

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = a
G := f b = a
H5 := f x0 = b
    x = y

%PhoX% elim H with x0.
2 goals created.

goal 2/4
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = a
G := f b = a
H5 := f x0 = b
H6 := x0 = b
    x = y

goal 1/4
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = a
G := f b = a
H5 := f x0 = b
H6 := x0 = a
    x = y

%PhoX% intro.
0 goal created.

goal 3/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = b
    x = y

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = a
G := f b = a
H5 := f x0 = b
H6 := x0 = b
    x = y

%PhoX% intro.
0 goal created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
    x = y

%PhoX% prove f b = b.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
G := f b = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
    f b = b

%PhoX% intro.
0 goal created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
G := f b = b
    x = y

%PhoX% elim H0 with a.
1 goal created.

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
G := f b = b
H5 := f x0 = a
    x = y

%PhoX% elim H with x0.
2 goals created.

goal 2/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
G := f b = b
H5 := f x0 = a
H6 := x0 = b
    x = y

goal 1/3
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
G := f b = b
H5 := f x0 = a
H6 := x0 = a
    x = y

%PhoX% intro.
0 goal created.

goal 2/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = b
    x = y

goal 1/2
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = a
H4 := f a = b
G := f b = b
H5 := f x0 = a
H6 := x0 = b
    x = y

%PhoX% intro.
0 goal created.

goal 1/1
H := au_plus_deux
H0 := surj f
H1 := f x = f y
H2 := x = b
H3 := y = b
    x = y

%PhoX% intro.
0 goal created.

%PhoX% save th.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
th = au_plus_deux  inj f  surj f : theorem

bye