From adfa07525e071b2a47aed37dac276aa38c10099d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 20 Dec 2016 19:15:12 +0100
Subject: [PATCH] show na_own_acc

---
 theories/base_logic/lib/na_invariants.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index e9084a60c..61d22f6f0 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -53,6 +53,13 @@ Section proofs.
     intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
   Qed.
 
+  Lemma na_own_acc E2 E1 tid :
+    E2 ⊆ E1 → na_own tid E1 -∗ na_own tid E2 ∗ (na_own tid E2 -∗ na_own tid E1).
+  Proof.
+    intros HF. assert (E1 = E2 ∪ (E1 ∖ E2)) as -> by exact: union_difference_L.
+    rewrite na_own_union; last by set_solver+. iIntros "[$ $]". auto.
+  Qed.
+
   Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
   Proof.
     iIntros "HP".
-- 
GitLab