proposition: Lemma merge_same (F : graph) (h k: equiv_rel F) (i i' o o': F): (h =2 k) -> h i i' -> h o o' -> point (merge F h) (\pi i) (\pi o) ≃2 point (merge F k) (\pi i') (\pi o').
proof: Proof. intros H Hi Ho. Iso2 (merge_same' H); rewrite merge_same'E =>//; apply /eqquotP; by rewrite <- H. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)