proposition: Lemma open_add_vertexE : ((forall a, open_add_vertex a (@inj_v (G ∔ a)%G2 (inr tt)) = fresh (vset (open G))) *(forall a x, open_add_vertex a (@inj_v (G ∔ a)%G2 (inl x)) = @inj_v G x))%type.
proof: Proof. split => [a|a x]. - rewrite /vfun_of/= vfun_bodyE. exact: inj_v_open. move => H /=. by rewrite imfset_bij_bwdE. - rewrite /vfun_of/= vfun_bodyE. exact: inj_v_open. move => H /=. by rewrite imfset_bij_bwdE. Qed.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)