>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