proposition: Lemma merge_merge (G: graph) (h k: pairs G) (k': pairs (merge_seq G h)) (i o: G): k' = map_pairs (pi (eqv_clot h)) k -> point (merge_seq (merge_seq G h) k') (\pi (\pi i)) (\pi (\pi o)) ≃2 point (merge_seq G (h++k)) (\pi i) (\pi o).
proof: Proof. intro K. Iso2 (merge_merge_seq K); by rewrite /=merge_merge_seqE. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)