proposition: Theorem binds_dec : forall A x (v : A) (E : gen_env A), (forall w w' : A, { w = w' } + { ¬ w = w' }) -> { x ∹ v ⋲ E } + { ¬ x ∹ v ⋲ E }.
proof: Proof. intros A x v E Hdec. elim binds_dec_exists with A x E; intro Hdec2. destruct Hdec2 as [ w Hbind ]. elim (Hdec v w); intro Hneq; subst. left; auto. right. intro. assert (v = w) by (apply binds_eq_inv with x E; auto). auto. right; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv