From 1a0c58608d445f93e50e175016d3d130b6220984 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Jun 2019 11:57:09 +0200
Subject: [PATCH] Add lemma `meta_token_difference`.

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

diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index a3b687fea..4ae299548 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -267,6 +267,13 @@ Section gen_heap.
     iIntros "[Hm1 Hm2]". by iApply (meta_token_union_2 with "Hm1 Hm2").
   Qed.
 
+  Lemma meta_token_difference l E1 E2 :
+    E1 ⊆ E2 → meta_token l E2 ⊣⊢ meta_token l E1 ∗ meta_token l (E2 ∖ E1).
+  Proof.
+    intros. rewrite {1}(union_difference_L E1 E2) //.
+    by rewrite meta_token_union; last set_solver.
+  Qed.
+
   Lemma meta_agree `{Countable A} l i (x1 x2 : A) :
     meta l i x1 -∗ meta l i x2 -∗ ⌜x1 = x2⌝.
   Proof.
-- 
GitLab