From 6fa72b41e480e51a86e7abe772d4f19851cc5447 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 Sep 2020 11:07:50 +0200
Subject: [PATCH] add simpler ghost_var_agree lemma

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

diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index 66af6d3f7..32b9d2af6 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/theories/base_logic/lib/ghost_var.v
@@ -50,6 +50,13 @@ Section lemmas.
     iDestruct (own_valid_2 with "Hvar1 Hvar2") as %[Hq Ha]%frac_agree_op_valid.
     done.
   Qed.
+  (** Almost all the time, this is all you really need. *)
+  Lemma ghost_var_agree γ a1 q1 a2 q2 :
+    ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜a1 = a2⌝.
+  Proof.
+    iIntros "Hvar1 Hvar2".
+    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
+  Qed.
 
   (** This is just an instance of fractionality above, but that can be hard to find. *)
   Lemma ghost_var_split γ a q1 q2 :
-- 
GitLab