>PhoX> Sort term. Sort term defined >PhoX> def union U V x = (U x) (V x). union = \U,V,x (U x V x) : ('a prop) ('a prop) 'a prop >PhoX> def intervide U V = x ((U x) (V x)). intervide = \U,V x:U V x : ('a prop) ( 'a prop) prop >PhoX> def inclus A B = x ((A x) (B x)). inclus = \A,B x:A B x : ('a prop) ('a prop) prop >PhoX> Cst ouvert : (term prop) prop. ouvert : (term prop) prop >PhoX> def connexe A = U, V (ouvert U ouvert V (inclus A (union U >PhoX> V)) (intervide U V) (inclus A U) (inclus A V)). connexe = \A U,V (ouvert U ouvert V inclus A (union U V) intervide U V inclus A U inclus A V) : (term prop) prop >PhoX> goal >PhoX> A,B (connexe A connexe B x ((A x) (B x)) connexe (union A B)). Here is the goal: goal 1/1 A,B (connexe A connexe B x:A B x connexe (union A B)) %PhoX% intros. 1 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x connexe (union A B) %PhoX% intros. 1 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V inclus (union A B) U inclus (union A B) V %PhoX% prove inclus A (union U V). 2 goals created. goal 2/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) inclus (union A B) U inclus (union A B) V goal 1/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V inclus A (union U V) %PhoX% intros. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V H6 := A x union U V x %PhoX% elim H4. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V H6 := A x union A B x %PhoX% intro l. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V H6 := A x A x %PhoX% axiom H6. 0 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) inclus (union A B) U inclus (union A B) V %PhoX% prove inclus B (union U V). 2 goals created. goal 2/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) inclus (union A B) U inclus (union A B) V goal 1/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) inclus B (union U V) %PhoX% intros. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) H6 := B x union U V x %PhoX% elim H4. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) H6 := B x union A B x %PhoX% intro r. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) H6 := B x B x %PhoX% axiom H6. 0 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) inclus (union A B) U inclus (union A B) V %PhoX% apply H with H2 and H3 and G and H5. 1 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) G1 := inclus A U inclus A V inclus (union A B) U inclus (union A B) V %PhoX% apply H0 with H2 and H3 and G0 and H5. 1 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) G1 := inclus A U inclus A V G2 := inclus B U inclus B V inclus (union A B) U inclus (union A B) V %PhoX% left G1. 2 goals created. goal 2/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) G2 := inclus B U inclus B V H6 := inclus A U inclus (union A B) U inclus (union A B) V goal 1/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) G2 := inclus B U inclus B V H6 := inclus A V inclus (union A B) U inclus (union A B) V %PhoX% left G2. 2 goals created. goal 2/3 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U inclus (union A B) U inclus (union A B) V goal 1/3 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B V inclus (union A B) U inclus (union A B) V %PhoX% intro r. 1 goal created. goal 1/3 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B V inclus (union A B) V %PhoX% intros. 1 goal created. goal 1/3 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B V H8 := union A B x V x %PhoX% left H8. 2 goals created. goal 2/4 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B V H8 := A x V x goal 1/4 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B V H8 := B x V x %PhoX% elim H7. 1 goal created. goal 1/4 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B V H8 := B x B x %PhoX% axiom H8. 0 goal created. goal 3/3 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) G2 := inclus B U inclus B V H6 := inclus A U inclus (union A B) U inclus (union A B) V goal 2/3 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U inclus (union A B) U inclus (union A B) V goal 1/3 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B V H8 := A x V x %PhoX% elim H6. 1 goal created. goal 1/3 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B V H8 := A x A x %PhoX% axiom H8. 0 goal created. goal 2/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) G2 := inclus B U inclus B V H6 := inclus A U inclus (union A B) U inclus (union A B) V goal 1/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U inclus (union A B) U inclus (union A B) V %PhoX% left H1. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U H1 := A x B x inclus (union A B) U inclus (union A B) V %PhoX% left H1. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U H1 := A x H8 := B x inclus (union A B) U inclus (union A B) V %PhoX% elim H5. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U H1 := A x H8 := B x x0:U V x0 %PhoX% intro 2. 2 goals created. goal 2/3 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U H1 := A x H8 := B x V ?1 goal 1/3 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U H1 := A x H8 := B x U ?1 %PhoX% elim H7. 1 goal created. goal 1/3 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U H1 := A x H8 := B x B ?1 %PhoX% axiom H8. 0 goal created. goal 2/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) G2 := inclus B U inclus B V H6 := inclus A U inclus (union A B) U inclus (union A B) V goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U H1 := A x H8 := B x V x %PhoX% elim H6. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A V H7 := inclus B U H1 := A x H8 := B x A x %PhoX% axiom H1. 0 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) G2 := inclus B U inclus B V H6 := inclus A U inclus (union A B) U inclus (union A B) V %PhoX% left G2. 2 goals created. goal 2/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U inclus (union A B) U inclus (union A B) V goal 1/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V inclus (union A B) U inclus (union A B) V %PhoX% left H1. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V H1 := A x B x inclus (union A B) U inclus (union A B) V %PhoX% left H1. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V H1 := A x H8 := B x inclus (union A B) U inclus (union A B) V %PhoX% elim H5. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V H1 := A x H8 := B x x0:U V x0 %PhoX% intro 2. 2 goals created. goal 2/3 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V H1 := A x H8 := B x V ?2 goal 1/3 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V H1 := A x H8 := B x U ?2 %PhoX% elim H6. 1 goal created. goal 1/3 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V H1 := A x H8 := B x A ?2 %PhoX% axiom H1. 0 goal created. goal 2/2 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U inclus (union A B) U inclus (union A B) V goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V H1 := A x H8 := B x V x %PhoX% elim H7. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B V H1 := A x H8 := B x B x %PhoX% axiom H8. 0 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U inclus (union A B) U inclus (union A B) V %PhoX% intro l. 1 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x:A B x H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U inclus (union A B) U %PhoX% intros. 1 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U H8 := union A B x U x %PhoX% left H8. 2 goals created. goal 2/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U H8 := A x U x goal 1/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U H8 := B x U x %PhoX% elim H7. 1 goal created. goal 1/2 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U H8 := B x B x %PhoX% axiom H8. 0 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U H8 := A x U x %PhoX% elim H6. 1 goal created. goal 1/1 H := connexe A H0 := connexe B H1 := x0:A B x0 H2 := ouvert U H3 := ouvert V H4 := inclus (union A B) (union U V) H5 := intervide U V G := inclus A (union U V) G0 := inclus B (union U V) H6 := inclus A U H7 := inclus B U H8 := A x A x %PhoX% axiom H8. 0 goal created. %PhoX% save th. Building proof .... Typing proof .... Verifying proof .... Saving proof .... th = A,B (connexe A connexe B x:A B x connexe (union A B)) : theorem bye