diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 4a72231c01cebf869f5a315a9b73d34377e1489a..22c010f755346a4106394718fad590e2b76e6cf2 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -276,7 +276,6 @@ Proof.
     eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
-
 End box.
 
 Typeclasses Opaque slice box.
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 5edcb5d02a6c483c55d385bae46f1b4000f67ffa..2d0ebc3975a3ef21cf54ffaf291abe4e2a8675e4 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -330,6 +330,9 @@ Proof. done. Qed.
 Global Instance from_or_bupd P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
+Global Instance from_or_later P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /FromOr=><-. apply or_elim; apply later_mono; auto with I. Qed.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.