proposition: Lemma add_vlabel_two a b (x: unit+unit) c: two_graph a b [tst x <- c] ≃ two_graph (if x then a⊗c else a) (if x then b else b⊗c).
proof: Proof. case x; case=>/=. etransitivity. apply iso_sym. apply union_add_vlabel_l. apply union_iso=>//. apply add_vlabel_unit. etransitivity. apply iso_sym. apply union_add_vlabel_r. apply union_iso=>//. apply add_vlabel_unit. Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)