diff --git a/iris/lifting.v b/iris/lifting.v
index 7e36e3913d6611223515c876eb45653e323797a9..8526f16e4ed5c1f40b3be94613969edee30fa107 100644
--- a/iris/lifting.v
+++ b/iris/lifting.v
@@ -11,6 +11,7 @@ Context {Σ : iParam}.
 Implicit Types v : ival Σ.
 Implicit Types e : iexpr Σ.
 Implicit Types σ : istate Σ.
+Transparent uPred_holds.
 
 Lemma wp_lift_step E1 E2
     (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) Q e1 σ1 :
diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v
index ced05a0cb03e52be02224f8d714b3affcc82407d..2e83581e4ebd8cd3bb40cfdff8105749fa8d3c7f 100644
--- a/iris/pviewshifts.v
+++ b/iris/pviewshifts.v
@@ -30,6 +30,7 @@ Section pvs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
 Implicit Types m : icmra' Σ.
+Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
 Proof.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 15bb4639efeef37b23c6c66e02a5524ea3d91217..3e34864facf61be6f6578060083622cb1563ce06 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -58,6 +58,7 @@ Implicit Types P : iProp Σ.
 Implicit Types Q : ival Σ → iProp Σ.
 Implicit Types v : ival Σ.
 Implicit Types e : iexpr Σ.
+Transparent uPred_holds.
 
 Lemma wp_weaken E1 E2 e Q1 Q2 r n n' :
   E1 ⊆ E2 → (∀ v r n', n' ≤ n → ✓{n'} r → Q1 v n' r → Q2 v n' r) →
diff --git a/modures/logic.v b/modures/logic.v
index dcab3b5043db5f5660ec27e14f18ba55277c0d16..e9b058004387d504d26062b8098abf09f30b655e 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -11,6 +11,8 @@ Record uPred (M : cmraT) : Type := IProp {
     uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
 }.
 Arguments uPred_holds {_} _ _ _ : simpl never.
+Global Opaque uPred_holds.
+Local Transparent uPred_holds.
 Hint Resolve uPred_0.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.