proposition: Lemma merge_iso2 (F G : graph) (h: F ≃ G) l (i o: F): point (merge_seq F l) (\pi i) (\pi o) ≃2 point (merge_seq G (map_pairs h l)) (\pi (h i)) (\pi (h o)).
proof: Proof. Iso2 (merge_iso h l); by rewrite h_mergeE. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)