Let `iNext` detect equalities `Next x ≡ Next y`.

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.

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.