proposition: Theorem binds_update_self : forall A x (v : A) (F : gen_env A), x ∈ F -> x ∹ v ⋲ (F ::= (x ∶ v)).
proof: Proof. intros A x v F Hin. rewrite update_update_one. apply binds_update_one_eq; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv