proposition: Theorem binds_dec_exists : forall A x (E : gen_env A), { v | x ∹ v ⋲ E } + { forall v, ¬ x ∹ v ⋲ E }.
proof: Proof. intros A x E. unfold binds. elim get_dec with A x E; intro Hget; [ left | right ]; auto. intro v. rewrite Hget. intro Heq. inversion Heq. Qed.
imports: Utf8 Equalities CoreGenericEnv