proposition: Lemma exercise6_4 g a b x: let comm F G b := F (G b) = G (F b) in equivalence g -> sgraph a -> sgraph b -> substrate g = x -> sub a g -> [/\ (domain a = x -> g \cg a = g), (range a = x -> a \cg g = g), (domain a = x -> comm (composeg^~a) (intersection2 g) b) & (range a = x -> comm (composeg a) (intersection2 g) b)].
proof: Proof. move=> comm eg ga gb sg ag. have gg: sgraph g by fprops. split. + move=> ax; set_extens y. move /compg_P=> [py [z J1a J2g]]. move: (ag _ J1a) => J1g. rewrite - py; equiv_tac. move=> yg; move: (gg _ yg)=> py; apply/compg_P. split =>//. have : (inc (P y) (domain a)) by rewrite ax - sg; substr_tac. move/(domainP ga)=> [z Ja]; exists z =>//. move: (ag _ Ja)=> Jg. have J2g:inc (J z (P y)) g by equiv_tac. rewrite - py in yg; equiv_tac. + move=> ax; rewrite /comp; set_extens y. move /compg_P => [py [z J1g J2a]]. move: (ag _ J2a) => J2g. rewrite - py; equiv_tac. move=> yg; move: (gg _ yg)=> py; apply/compg_P =>//. have : (inc (Q y) (range a)) by rewrite ax - sg; substr_tac. move/(rangeP ga); move=> [z Ja]; split => //;exists z =>//. move: (ag _ Ja)=> Jg. have J2g:inc (J (Q y) z) g by equiv_tac. rewrite - py in yg; equiv_tac. + move=> ax; set_extens y. move /compg_P => [py [z J1a/setI2_P [J2g J3b]]]; apply/setI2_i. move: (ag _ J1a) => J1g; rewrite - py; equiv_tac. apply/compg_P;split=>//;exists z=>//. move=> /setI2_P [yg] /compg_P [py [z J1a J2b]]. apply/compg_P; split => //; exists z => //; apply:setI2_i => //. move: (ag _ J1a)=> Jg. have J2g:inc (J z (P y)) g by equiv_tac. rewrite - py in yg; equiv_tac. + move=> ax; set_extens y. move /compg_P => [py [z /setI2_P [J2g J3b] J1a]]; apply/setI2_i. move: (ag _ J1a) => J1g; rewrite - py; equiv_tac. apply/compg_P;split=>//;exists z =>//. move=> /setI2_P [yg] /compg_P [py [z J1a J2b]]. apply/compg_P; split => //; exists z => //; apply:setI2_i => //. move: (ag _ J2b)=> Jg. have J2g:inc (J (Q y) z) g by equiv_tac. rewrite - py in yg; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)