diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index b1245dd5f149d65bb86fc0d1407aaf0402017e20..77ac1531037c1a983ef01a68e470237d796104ef 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -84,6 +84,12 @@ Section instances.
     iExists P. iFrame. iIntros "!> HP". iApply "HQ". iApply "HQ1". done.
   Qed.
 
+  Lemma make_laterable_mono Q1 Q2 :
+    (Q1 ⊢ Q2) → (make_laterable Q1 ⊢ make_laterable Q2).
+  Proof.
+    intros HQ12. iApply make_laterable_wand. rewrite HQ12. by iIntros "!# ?".
+  Qed.
+
   Global Instance make_laterable_laterable Q :
     Laterable (make_laterable Q).
   Proof.
@@ -97,6 +103,8 @@ Section instances.
     iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
   Qed.
 
+  (** Written internally (as an entailment of wands) to reflect
+      that persistent assertions can be kept unchanged. *)
   Lemma make_laterable_intro P Q :
     Laterable P →
     □ (◇ P -∗ Q) -∗ P -∗ make_laterable Q.