Commit 4e59a653 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove ownM_something.

It is unused, and ownM_empty is stronger.
parent 406637f4
...@@ -1128,8 +1128,6 @@ Proof. ...@@ -1128,8 +1128,6 @@ Proof.
split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl. split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
rewrite -(persistent_core a). by apply cmra_core_monoN. rewrite -(persistent_core a). by apply cmra_core_monoN.
Qed. Qed.
Lemma ownM_something : True a, uPred_ownM a.
Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
Lemma ownM_empty : True uPred_ownM . Lemma ownM_empty : True uPred_ownM .
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed. Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment