diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 8686bc3939499f0341591c34997b63a274069874..e1c324096dbb1f37b9d3f34de057d45cf4a5987f 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -17,7 +17,7 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 (* Own and valid derived *)
 Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
 Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
-Lemma affinely_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
   rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
     [by rewrite persistently_elim|].
@@ -31,7 +31,7 @@ Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
 Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
 Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
-Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma intuitionistically_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
   rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
     first by rewrite persistently_elim.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 4de962442ec86acc4008d9eba0aefe813c745153..4e0df1b95d65efe7085bfc9cbe4ce19694a9f4df 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -503,6 +503,11 @@ Lemma monPred_at_affinely i P : (<affine> P) i ⊣⊢ <affine> (P i).
 Proof. by rewrite /bi_affinely monPred_at_and monPred_at_emp. Qed.
 Lemma monPred_at_affinely_if i p P : (<affine>?p P) i ⊣⊢ <affine>?p (P i).
 Proof. destruct p=>//=. apply monPred_at_affinely. Qed.
+Lemma monPred_at_intuitionistically i P : (□ P) i ⊣⊢ □ (P i).
+Proof. by rewrite /bi_intuitionistically monPred_at_affinely monPred_at_persistently. Qed.
+Lemma monPred_at_intuitionistically_if i p P : (□?p P) i ⊣⊢ □?p (P i).
+Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.
+
 Lemma monPred_at_absorbingly i P : (<absorb> P) i ⊣⊢ <absorb> (P i).
 Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
 
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 826536997118a0d416e3bd1bd79fe29a3b2a58a8..d3a495e55394c305da4ed7864d399cc660d7fe5f 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -61,7 +61,7 @@ Global Instance from_modal_persistently_monPred_at `(sel : A) P Q 𝓠 i :
 Proof.
   rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
 Qed.
-Global Instance from_modal_affinely_persistently_monPred_at `(sel : A) P Q 𝓠 i :
+Global Instance from_modal_intuitionistically_monPred_at `(sel : A) P Q 𝓠 i :
   FromModal modality_intuitionistically sel P Q → MakeMonPredAt i Q 𝓠 →
   FromModal modality_intuitionistically sel (P i) 𝓠 | 0.
 Proof.
@@ -101,6 +101,9 @@ Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
 Global Instance make_monPred_at_affinely i P 𝓟 :
   MakeMonPredAt i P 𝓟 → MakeMonPredAt i (<affine> P) (<affine> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_affinely=><-. Qed.
+Global Instance make_monPred_at_intuitionistically i P 𝓟 :
+  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (□ P) (□ 𝓟).
+Proof. by rewrite /MakeMonPredAt monPred_at_intuitionistically=><-. Qed.
 Global Instance make_monPred_at_absorbingly i P 𝓟 :
   MakeMonPredAt i P 𝓟 → MakeMonPredAt i (<absorb> P) (<absorb> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_absorbingly=><-. Qed.
@@ -112,6 +115,10 @@ Global Instance make_monPred_at_affinely_if i P 𝓟 p :
   MakeMonPredAt i P 𝓟 →
   MakeMonPredAt i (<affine>?p P) (<affine>?p 𝓟).
 Proof. destruct p; simpl; apply _. Qed.
+Global Instance make_monPred_at_intuitionistically_if i P 𝓟 p :
+  MakeMonPredAt i P 𝓟 →
+  MakeMonPredAt i (□?p P) (□?p 𝓟).
+Proof. destruct p; simpl; apply _. Qed.
 Global Instance make_monPred_at_embed i 𝓟 : MakeMonPredAt i ⎡𝓟⎤ 𝓟.
 Proof. by rewrite /MakeMonPredAt monPred_at_embed. Qed.
 Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) ⌜i ⊑ j⌝.