proposition: Theorem all_binds_single_empty : forall A x (v : A), (x ∶ v) ⊏ (@empty A) -> False.
proof: Proof. intros A x v Habind. apply all_binds_binds in Habind. apply binds_empty in Habind; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv