diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index 66af6d3f71a098df63530a1eb4e5f0ddf13e34d8..32b9d2af68614f9831ba1101a798e855be29a9b1 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 :