proposition: Theorem binds_update_notin : forall A x (v : A) (F G : gen_env A), x ∹ v ⋲ F -> x ∉ G -> x ∹ v ⋲ (F ::= G).
proof: Proof. intros A x v F G Hbind Hnotin. induction G as [ | G y w ] using env_ind. rewrite update_empty_r; auto. rewrite update_concat_r. rewrite update_update_one. apply notin_concat_inv in Hnotin. destruct Hnotin as [ HnotinG Hneq ]. apply notin_single_inv in Hneq. apply binds_update_one_neq; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv