proposition: Lemma merge_step (G' G H: graph2) (l : pairs (G+H)) : admissible_l l -> step G G' -> steps (point (merge_seq (G ⊎ H) l) (\pi (unl input)) (\pi (unr output))) (point (merge_seq (G' ⊎ H) (replace_ioL l)) (\pi (unl input)) (\pi (unr output))).
proof: Proof. move => A B. destruct B. - refine (cons_iso_steps _ (merge_add_vertexL A)). apply (one_step (step_v0 _ _)). - refine (cons_iso_steps _ (merge_add_edgeL _ _ _)). refine (cons_iso_steps _ (add_edge2_iso (merge_add_vertexL A) _ _ _)). rewrite 2!merge_add_vertexLE. refine (cons_step_steps _ (step_v1 _ _ _)). apply iso_step. symmetry. apply merge_add_vlabelL. - refine (cons_iso_steps _ (merge_add_edgeL _ _ _)). refine (cons_iso_steps _ (add_edge2_iso (merge_add_edgeL _ _ _) _ _ _)). rewrite !merge_add_edgeLE. refine (cons_iso_steps _ (add_edge2_iso (add_edge2_iso (merge_add_vertexL A) _ _ _) _ _ _)). do 4 rewrite {1}merge_add_vertexLE. refine (cons_step_steps _ (step_v2 _ _ _ _ _)). apply iso_step. symmetry. apply merge_add_edgeL. - refine (cons_iso_steps _ (merge_add_edgeL _ _ _)). refine (cons_step_steps _ (step_e0 _ _)). apply iso_step. etransitivity. symmetry. apply merge_add_vlabelL. by rewrite replace_ioE. - refine (cons_iso_steps _ (merge_add_edgeL _ _ _)). refine (cons_iso_steps _ (add_edge2_iso (merge_add_edgeL _ _ _) _ _ _)). rewrite !merge_add_edgeLE. refine (cons_step_steps _ (step_e2 _ _ _ _)). apply iso_step. etransitivity. symmetry. apply (merge_add_edgeL (u:=u∥v)). by rewrite replace_ioE. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)