proposition: Lemma merge2_merge (G: graph2) (h k: pairs G) (k': pairs (merge_seq G h)): k' = map_pairs (pi (eqv_clot h)) k -> merge2_seq (merge2_seq G h) k' ≃2 merge2_seq G (h++k).
proof: Proof. apply merge_merge. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)