proposition: Theorem binds_empty : forall A x (v : A), x ∹ v ⋲ (@empty A) -> False.
proof: Proof. intros A x v Hbind. inversion Hbind as [ Hget ]. rewrite get_empty in Hget. inversion Hget. Qed.
imports: Utf8 Equalities CoreGenericEnv