proposition: Lemma union_add_vlabel_r F G x a: F ⊎ G [tst x <- a] ≃ (F ⊎ G) [tst unr x <- a].
proof: Proof. etransitivity. apply union_C. etransitivity. apply union_add_vlabel_l. etransitivity. apply (add_vlabel_iso (union_C _ _)). reflexivity. Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)