Prove core ∅ ≡ ∅.

ecff0735 · Robbert Krebbers · edc30b17 · ecff0735
Commit ecff0735 authored May 22, 2016 by Robbert Krebbers
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -344,6 +344,8 @@ Section unit.
  Proof. by intros x; rewrite (comm op) left_id. Qed.
  Global Instance cmra_unit_persistent : Persistent ∅.
  Proof. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed.
+  Lemma cmra_core_unit : core (∅:A) ≡ ∅.
+  Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
 End unit.

 (** ** Local updates *)