diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index b0e3d4b1cd4cf8b45b9f8839d91147ea7b84883b..86fb2d25e2ade141f6f9f1072861d42add2a7803 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -144,7 +144,7 @@ Section heap.
   Lemma heap_mapsto_agree l q1 q2 v1 v2 :
     l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
-    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
     eapply pure_elim; [done|]=> /auth_own_valid /=.
     rewrite op_singleton pair_op singleton_valid. case.
     rewrite /= to_agree_comp_valid=>? Heq. fold_leibniz. eauto.