proposition: Theorem binds_belongs : forall A x (v : A) (F : gen_env A), x ∹ v ⋲ F -> x ∈ F.
proof: Proof. induction F using env_ind; intro Hbind. apply binds_empty in Hbind; inversion Hbind. apply binds_concat_inv in Hbind. destruct Hbind as [ Hbind | [ Hnotin Hbind ] ]. apply belongs_concat_r. unfold binds in Hbind. apply get_single_eq_inv in Hbind. destruct Hbind. apply belongs_single; auto. apply IHF in Hbind. apply belongs_concat_l; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv