diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 9953ed04bf3ed397da4b8ba4966295d2fc66b59e..c7fadbd22224237ba96e335c9372538df96626ff 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -385,6 +385,8 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /sbi_except_0 -later_or False_or. Qed.
+Lemma except_0_into_later P : ◇ P ⊢ ▷ P.
+Proof. by rewrite -except_0_later -later_intro. Qed.
 Lemma except_0_persistently P : ◇ <pers> P ⊣⊢ <pers> ◇ P.
 Proof.
   by rewrite /sbi_except_0 persistently_or -later_persistently persistently_pure.