proposition: Lemma dot2unit_r (G: graph2) a: G · unit_graph2 a ≃2 G [tst output <- a].
proof: Proof. irewrite (merge_iso2 (union_iso iso_id (add_vlabel2_unit' output _))). simpl. etransitivity. refine (merge_iso2 (union_add_vlabel_r _ _ _) _ _ _). simpl. etransitivity. refine (iso_iso2 (merge_add_vlabel _ _ _) _ _). simpl. etransitivity. refine (iso_iso2 (add_vlabel_iso (merge_union_K_l (K:=g2_one) (unl input) (unl output) (k:=fun _ => output) _ _ _) _ _) _ _)=>//. case; apply /eqquotP; eqv. simpl. rewrite !merge_union_KE/=. etransitivity. refine (add_vlabel2_iso (merge2_nothing _) _ _). repeat (constructor=>//). destruct G=>/=. by rewrite merge_nothingE. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)