Commit 65171af2 authored by Robbert Krebbers's avatar Robbert Krebbers

Alternative version of ownM_empty.

parent 1aac61c4
......@@ -1257,6 +1257,8 @@ Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
Proof. by intros; rewrite ownM_valid valid_elim. Qed.
Global Instance ownM_mono : Proper (flip () ==> ()) (@uPred_ownM M).
Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
Lemma ownM_empty' : uPred_ownM True.
Proof. apply (anti_symm _); auto using ownM_empty. Qed.
(* Viewshifts *)
Lemma rvs_intro P : P =r=> P.
......
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