From ee8815c0e53990c4c8f781e57d37d91ecfa2dead Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 21 Jun 2019 13:10:12 +0200
Subject: [PATCH] =?UTF-8?q?Have=20`iNext`=20turn=20`Next=20x=20=E2=89=A1?=
 =?UTF-8?q?=20Next=20y`=20into=20`x=20=E2=89=A1=20y`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/class_instances_sbi.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 56586ce3a..bda75b778 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -567,6 +567,14 @@ Proof.
   move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
 Qed.
 
+Global Instance into_laterN_Next {A : ofeT} only_head n n' (x y : A) :
+  NatCancel n 1 n' 0 →
+  IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
+Proof.
+  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
+  move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
+Qed.
+
 Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
   IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
   IntoLaterN false n (P1 ∧ P2) (Q1 ∧ Q2) | 10.
-- 
GitLab