proposition: Lemma exercise6_6b G H: equivalence G -> equivalence H -> substrate G = substrate H -> substrate (G \cg H) = substrate G.
proof: Proof. move=> eG eH sG. set_extens x. have xx:sgraph (G \cg H) by fprops. case /setU2_P; [move /(domainP xx) | move /(rangeP xx)]; move => [z] /compg_pP [t ta tb]; [rewrite sG | ] ; substr_tac. move=> xsG. have p3: related (G \cg H) x x. apply/compg_pP; exists x;equiv_tac => //; ue. substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)