diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index 9e2758efd58b32cf71f3322ba19c13f1d2f91c7c..21d496480cba966e277b3acf3d6189dd4bcf6f40 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -8,6 +8,15 @@ From iris Require Import options.
 Section upred.
 Context {M : ucmraT}.
 
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢@{uPredI M} ✓ x.1 ∧ ✓ x.2.
+Proof. by uPred.unseal. Qed.
+Lemma option_validI {A : cmraT} (mx : option A) :
+  ✓ mx ⊣⊢@{uPredI M} match mx with Some x => ✓ x | None => True : uPred M end.
+Proof. uPred.unseal. by destruct mx. Qed.
+Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) :
+  ✓ g ⊣⊢@{uPredI M} ∀ i, ✓ g i.
+Proof. by uPred.unseal. Qed.
+
 Section gmap_ofe.
   Context `{Countable K} {A : ofeT}.
   Implicit Types m : gmap K A.
@@ -26,10 +35,10 @@ Section gmap_cmra.
   Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢@{uPredI M} ✓ x.
   Proof.
     rewrite gmap_validI. apply: anti_symm.
-    - rewrite (bi.forall_elim i) lookup_singleton uPred.option_validI. done.
+    - rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
     - apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
-      + rewrite lookup_singleton uPred.option_validI. done.
-      + rewrite lookup_singleton_ne // uPred.option_validI.
+      + rewrite lookup_singleton option_validI. done.
+      + rewrite lookup_singleton_ne // option_validI.
         apply bi.True_intro.
   Qed.
 End gmap_cmra.
@@ -241,7 +250,7 @@ Section gmap_view.
       ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
   Proof.
     rewrite /gmap_view_frag -view_frag_op view_frag_validI.
-    rewrite singleton_op singleton_validI -pair_op uPred.prod_validI /=.
+    rewrite singleton_op singleton_validI -pair_op prod_validI /=.
     apply bi.and_mono; first done.
     rewrite agree_validI agree_equivI. done.
   Qed.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 8f86b9c0210e0dbb9dcd159e44db8d77b0916960..fa2327ae6c0df8517ad05bc054e38aaf5a0ab694 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -215,15 +215,8 @@ Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ ✓ a.
 Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. exact: uPred_primitive.prod_validI. Qed.
-Lemma option_validI {A : cmraT} (mx : option A) :
-  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-Proof. exact: uPred_primitive.option_validI. Qed.
 Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof. exact: uPred_primitive.discrete_valid. Qed.
-Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
-Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
 
 (** This is really just a special case of an entailment
 between two [siProp], but we do not have the infrastructure
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 2c628c6c423411c83b201cf02ef446e55e36d2d2..b3e6fb96c443918315c65857e8aeaa7bbc75c498 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -863,18 +863,9 @@ Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
 
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. by unseal. Qed.
-Lemma option_validI {A : cmraT} (mx : option A) :
-  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-Proof. unseal. by destruct mx. Qed.
-
 Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
 
-Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
-Proof. by unseal. Qed.
-
 (** This is really just a special case of an entailment
 between two [siProp], but we do not have the infrastructure
 to express the more general case. This temporary proof rule will