diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 46f2713441c52f03d802abf80ff1a3330d245829..fc0116733db7bcbbc00d1c75f9cde4500fc748a8 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -159,9 +159,14 @@ Proof. by rewrite /FromModal /= -bupd_intro. Qed.
 Global Instance from_modal_fupd E P `{!BiFUpd PROP} :
   FromModal modality_id (|={E}=> P) (|={E}=> P) P.
 Proof. by rewrite /FromModal /= -fupd_intro. Qed.
-Global Instance from_modal_step_fupdN E n P `{!BiFUpd PROP} :
-  FromModal (modality_laterN n) (|={E}â–·=>^n P) (|={E}â–·=>^n P) P.
-Proof. by rewrite /FromModal /= -step_fupdN_laterN. Qed.
+Global Instance from_modal_step_fupdN Ei Eo n P `{!BiFUpd PROP} :
+  (* Some cases in which [Ei ⊆ Eo] holds *)
+  TCOr (TCEq Ei Eo) (TCOr (TCEq Eo ⊤) (TCEq Ei ∅)) →
+  FromModal (modality_laterN n) (|={Eo}[Ei]â–·=>^n P) (|={Eo}[Ei]â–·=>^n P) P.
+Proof.
+  intros HE. rewrite /FromModal /= -step_fupdN_laterN //.
+  destruct HE as [->|[->| ->]]; set_solver+.
+Qed.
 
 Global Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
   ElimModal True p false (|==> P) P (|==> Q) (|==> Q).