proposition: Lemma exercise4_6 G: sgraph G -> (fgraph G <-> {when sgraph &, {morph (composeg ^~G) : H H' / H \cap H'}}).
proof: Proof. move => gG; split. move=> fG H H' _ _; set_extens x. move /compg_P => [px [y J1 /setI2_P [J2 J3]]]. apply: setI2_i; apply /compg_P; split => //;ex_tac. move /setI2_P => [] /compg_P [px [y J1 J2 /compg_P [_ [y' J1' J2']]]]. rewrite (fgraph_pr fG J1 J1') in J2. apply/compg_P; split => //; ex_tac; fprops. move=> hyp; split=>// x y xG yG Pxy. set (H:= singleton(J (Q x) (P x))). set (H':= singleton(J (Q y) (P y))). have gh: sgraph H by move=> t /set1_P ->; fprops. have gh': sgraph H' by move=> t /set1_P->; fprops. move: (gG _ xG)(gG _ yG)=> xp yp. rewrite - xp in xG. rewrite - yp in yG. apply: pair_exten=>//. have p1: inc (J (P x)(P x)) (H \cg G). apply /compg_P; split;fprops; aw;ex_tac; rewrite /H; fprops. have p2: inc (J (P y)(P y)) (H' \cg G). apply /compg_P; split;fprops; aw;ex_tac; rewrite /H'; fprops. have : (inc (J (P x)(P x)) ((H \cap H') \cg G)). by rewrite hyp//; apply: setI2_i => //;rewrite Pxy. move/compg_P => [_ [z _]]; aw. move /setI2_P => [] /set1_P r1 /set1_P r2. by rewrite -(pr1_def r1) -(pr1_def r2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)