Commit 653b8d3f authored by Ralf Jung's avatar Ralf Jung

no reason for this prime

parent 7d2f957d
......@@ -69,7 +69,7 @@ Lemma own_valid γ a : own i γ a ⊑ ✓ a.
Proof.
rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalC_validN.
Qed.
Lemma own_valid_r' γ a : own i γ a (own i γ a a).
Lemma own_valid_r γ a : own i γ a (own i γ a a).
Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
Global Instance own_timeless γ a : Timeless a TimelessP (own i γ a).
Proof. unfold own; apply _. 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