proposition: Lemma add_vlabel_iso'' F G (h: F ≃ G) x x' (ex: h x = x') a b (e: a ≡ b): F [tst x <- a] ≃ G [tst x' <- b].
proof: Proof. Iso h h.e h.d. split; try apply h. move=>v/=. rewrite -ex inj_eq=>/=. 2: by apply bij_injective. by case eq_op; rewrite ?e vlabel_iso. Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)