diff --git a/tests/proofmode.v b/tests/proofmode.v
index f657edfe7c92084191dc6dc285e6b1e0c55b7972..b92a17884c37fb343e42b2dad58dd43d58011b6c 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -377,6 +377,10 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
   (∀ y, ∃ x, ▷ Φ x y) -∗ ▷ (∀ y, ∃ x, Φ x y).
 Proof. iIntros "H". iNext. done. Qed.
 
+Lemma text_iNext_Next {A B : ofeT} (f : A -n> A) x y :
+  Next x ≡ Next y -∗ (Next (f x) ≡ Next (f y) : PROP).
+Proof. iIntros "H". iNext. by iRewrite "H". Qed.
+
 Lemma test_iFrame_persistent (P Q : PROP) :
   □ P -∗ Q -∗ <pers> (P ∗ P) ∗ (P ∗ Q ∨ Q).
 Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index bda75b7782e05a282d1a876de54395abb166d6ca..debfbfa98da9e6cb8815fc0cd1dcfb95e9136263 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -373,6 +373,11 @@ Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_laterN n P :
   FromModal (modality_laterN n) (â–·^n P) (â–·^n P) P.
 Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_Next {A : ofeT} (x y : A) :
+  FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
+    (▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
+Proof. by rewrite /FromModal /= later_equivI. Qed.
+
 Global Instance from_modal_except_0 P : FromModal modality_id (â—‡ P) (â—‡ P) P.
 Proof. by rewrite /FromModal /= -except_0_intro. Qed.