>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