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