proposition: Theorem belongs_binds : forall A x (F : gen_env A), x ∈ F -> exists v, x ∹ v ⋲ F.
proof: Proof. induction F as [ | F y w IHF ] using env_ind; intro Hbelong. apply belongs_empty in Hbelong. inversion Hbelong. destruct (eq_keys_dec x y) as [ Heq | Hneq ]. subst. exists w. apply binds_concat_r. apply binds_single; auto. apply belongs_concat_inv in Hbelong. destruct Hbelong as [ HinF | Hiny ]. apply IHF in HinF. destruct HinF as [ w' Hbind ]. exists w'. apply binds_concat_l; auto. apply notin_single; auto. apply belongs_single_inv in Hiny. contradiction. Qed.
imports: Utf8 Equalities CoreGenericEnv