diff --git a/algebra/frac.v b/algebra/frac.v
index 47fd97642304649210775ce3d4d22324fef5991f..2a10b1cd166c725eb0cc7a8498bed1632838ef46 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -1,6 +1,5 @@
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
 
 Notation frac := Qp (only parsing).
 
@@ -20,12 +19,6 @@ Qed.
 Canonical Structure fracR := discreteR frac frac_ra_mixin.
 End frac.
 
-(** Internalized properties *)
-Lemma frac_equivI {M} (x y : frac) : x ≡ y ⊣⊢ (x = y : uPred M).
-Proof. by uPred.unseal. Qed.
-Lemma frac_validI {M} (x : frac) : ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M).
-Proof. by uPred.unseal. Qed.
-
 (** Exclusive *)
 Global Instance frac_full_exclusive : Exclusive 1%Qp.
 Proof.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 2457a9577b084ff7878ee88dcd55b0e303e9bc60..597066ded0a206bd929ae9412eb29cc9c6ced61e 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -118,7 +118,7 @@ Section heap.
     rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //.
     apply (anti_symm (⊢)); last by apply pure_elim_l.
     rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
-    rewrite option_validI prod_validI frac_validI discrete_valid.
+    rewrite option_validI prod_validI !discrete_valid /=.
     by apply pure_elim_r.
   Qed.