proposition: Theorem binds_update_in : forall A x (v : A) (F G : gen_env A), x ∈ F -> x ∹ v ⋲ G -> x ∹ v ⋲ (F ::= G).
proof: Proof. intros A x v F G Hin Hbind. induction G as [ | G y w ] using env_ind. apply binds_empty in Hbind. inversion Hbind. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | Hnotin ]. apply binds_single_inv in Hbind. destruct Hbind; subst. apply (belongs_update G) in Hin. rewrite update_concat_r. rewrite update_update_one. apply binds_update_one_eq; auto. destruct Hnotin as [ Hnotin Hbind ]. apply notin_single_inv in Hnotin. rewrite update_concat_r. rewrite update_update_one. apply binds_update_one_neq; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv