diff --git a/_CoqProject b/_CoqProject
index c447a2bc4de6f5956033a7623b3c76c39d83309d..34b5eeb819c0dd1eae808bcb8716729595a3d4dc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,6 +27,7 @@ theories/lang/lib/new_delete.v
 theories/lang/lib/spawn.v
 theories/lang/lib/lock.v
 theories/lang/lib/arc.v
+theories/lang/lib/tests.v
 theories/typing/base.v
 theories/typing/type.v
 theories/typing/util.v
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
new file mode 100644
index 0000000000000000000000000000000000000000..135f2fe7c2fe3e05db5ff831864a75b893f43093
--- /dev/null
+++ b/theories/lang/lib/tests.v
@@ -0,0 +1,18 @@
+From iris.program_logic Require Import weakestpre.
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import lang proofmode notation.
+Set Default Proof Using "Type".
+
+Section tests.
+  Context `{!lrustG Σ}.
+
+  Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
+    {{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
+      #l1 = #l2 @ E
+    {{{ (b: bool), RET LitV (lit_of_bool b); (if b then ⌜l1 = l2⌝ else ⌜l1 ≠ l2⌝) ∗
+                                     l1 ↦{q1} v1 ∗ l2 ↦{q2} v2 }}}.
+  Proof.
+    iIntros (Φ) "[Hl1 Hl2] HΦ". wp_op; try (by eauto); [|];
+      intros ?; iApply "HΦ"; by iFrame.
+  Qed.
+End tests.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 436cdcaf31e9508659eac7b60805f84fe4f8c1a4..40d5c1497041cc8270f2b265b32bf66c41966777 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -278,13 +278,13 @@ Proof.
 Qed.
 
 Lemma wp_eq_loc E (l1 : loc) (l2: loc) P Φ :
+  (P -∗ ∃ q v, ▷ l1 ↦{q} v) →
+  (P -∗ ∃ q v, ▷ l2 ↦{q} v) →
   (l1 = l2 → P -∗ ▷ Φ (LitV true)) →
   (l1 ≠ l2 → P -∗ ▷ Φ (LitV false)) →
-  (P -∗ ∃ q v, l1 ↦{q} v) →
-  (P -∗ ∃ q v, l2 ↦{q} v) →
   P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
 Proof.
-  iIntros (Heq Hne Hl1 Hl2) "HP".
+  iIntros (Hl1 Hl2 Heq Hne) "HP".
   destruct (bool_decide_reflect (l1 = l2)).
   - rewrite Heq // {Heq Hne}. iApply wp_bin_op_pure; subst.
     + intros. apply BinOpEqTrue. constructor.
@@ -294,23 +294,26 @@ Proof.
     iSplitR.
     { iPureIntro. eexists _, _, _. constructor. apply BinOpEqFalse. by auto. }
     (* We need to do a little gymnastics here to apply Hne now and strip away a
-       â–· but also keep the P. *)
-    iAssert (P ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
-    { iSplit; first done. by iApply Hne. }
-    iNext.
+       ▷ but also have the ↦s. *)
+    iAssert ((▷ ∃ q v, l1 ↦{q} v) ∧ (▷ ∃ q v, l2 ↦{q} v) ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
+    { iSplit; last iSplit.
+      - iDestruct (Hl1 with "HP") as (??) "?". iNext. eauto.
+      - iDestruct (Hl2 with "HP") as (??) "?". iNext. eauto.
+      - by iApply Hne. }
+    clear Hne Hl1 Hl2. iNext.
     iIntros (e2 σ2 efs Hs) "!>".
     inv_head_step. iSplitR=>//.
     match goal with [ H : bin_op_eval _ _ _ _ _ |- _ ] => inversion H end;
       inv_lit=>//.
-    * iExFalso. iDestruct "HP" as "[HP _]".
-      iDestruct (Hl1 with "HP") as (??) "Hl1".
+    * iExFalso. iDestruct "HP" as "[Hl1 _]".
+      iDestruct "Hl1" as (??) "Hl1".
       iDestruct (heap_read σ2 with "Hσ1 Hl1") as (n') "%".
       simplify_eq.
-    * iExFalso. iDestruct "HP" as "[HP _]".
-      iDestruct (Hl2 with "HP") as (??) "Hl2".
+    * iExFalso. iDestruct "HP" as "[_ [Hl2 _]]".
+      iDestruct "Hl2" as (??) "Hl2".
       iDestruct (heap_read σ2 with "Hσ1 Hl2") as (n') "%".
       simplify_eq.
-    * iDestruct "HP" as "[_ $]". done.
+    * iDestruct "HP" as "[_ [_ $]]". done.
 Qed.
 
 Lemma wp_eq_loc_0_r E (l : loc) P Φ :