proposition: Lemma merge_nothing (F: graph) (h: pairs F) (i o: F): List.Forall (fun p => p.1 = p.2) h -> point (merge_seq F h) (\pi i) (\pi o) ≃2 point F i o.
proof: Proof. intros H. Iso2 (merge_nothing H); by rewrite merge_nothingE. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)