proposition: Lemma merge2_iso2 F G (h: F ≃2 G) l: merge2_seq F l ≃2 merge2_seq G (map_pairs h l).
proof: Proof. Iso2 (merge_iso h l); by rewrite h_mergeE ?iso2_input ?iso2_output. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)