diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index b638109f4e5327b23971b21d6d16f025fd7cf713..730dea755bb1781128723cfda4e7974166016a62 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1609,24 +1609,20 @@ Proof.
 Qed.
 
 Global Instance into_later_affinely n P Q :
-  MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterN false n (bi_affinely P) (bi_affinely Q).
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n (bi_affinely P) (bi_affinely Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
 Global Instance into_later_absorbingly n P Q :
-  MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q).
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
 Global Instance into_later_plainly n P Q :
-  MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterN false n (bi_plainly P) (bi_plainly Q).
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n (bi_plainly P) (bi_plainly Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
-  MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterN false n (bi_persistently P) (bi_persistently Q).
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n (bi_persistently P) (bi_persistently Q).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
 Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q :
-  MaybeIntoLaterN false n P Q → MaybeIntoLaterN false n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
+  IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index cfec41ed65338ce0d56722274db1102e6f98b9f2..b5a92ce017b925d5dd1ad261acab0cf421332a89 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -426,10 +426,10 @@ Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
 Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
 
 Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
-  MaybeIntoLaterN false n P Q → MakeMonPredAt i Q 𝓠 →
-  MaybeIntoLaterN false n (P i) 𝓠.
+  IntoLaterN false n P Q → MakeMonPredAt i Q 𝓠 →
+  IntoLaterN false n (P i) 𝓠.
 Proof.
-  rewrite /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
+  rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
    by rewrite monPred_at_later.
 Qed.
 Global Instance from_later_monPred_at i n P Q 𝓠 :