proposition: Lemma merge_union_K_l (F K: graph) (i o: F+K) (h: pairs (F+K)) (k: K -> F) (kv: forall x: K, vlabel x = 1) (ke: edge K -> False) (kh: forall x: K, unr x = unl (k x) %[mod (eqv_clot h)]): point (merge_seq (F ⊎ K) h) (\pi i) (\pi o) ≃2 point (merge_seq F (union_K_pairs h k)) (\pi (sum_left k i)) (\pi (sum_left k o)).
proof: Proof. Iso2 (merge_union_K kv kh ke)=>/=; by rewrite ?merge_union_KE. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)