proposition: Lemma merge_add_vertexL: point (merge_seq (G ∔ a ⊎ H) l) (\pi (inl (inl input))) (\pi (unr output)) ≃2 point (merge_seq (G ⊎ H) (replace_ioL l)) (\pi (unl input)) (\pi (unr output)) ∔ a.
proof: Proof. eapply iso2_comp. apply (iso_iso2' (h:=merge_iso (iso_sym (union_A _ _ _)) _)). 1,2: rewrite merge_isoE//. eapply iso2_comp. refine (iso_iso2' (h:=merge_iso (union_iso iso_id (union_C _ _)) _) _ _). 1,2: rewrite merge_isoE//. eapply iso2_comp. refine (iso_iso2' (h:=merge_iso (union_A _ _ _) _) _ _). 1,2: rewrite merge_isoE//. eapply iso2_sym. eapply iso2_comp. refine (iso_iso2' (h:=union_merge_l _ _) _ _). 1,2: rewrite union_merge_lEl//. eapply iso2_sym. apply merge_same'. by rewrite admissible_map. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)