From 74639a53fd2fd6a38834a96499a7e6a1b47c1c18 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 10 Dec 2018 10:37:04 +0100
Subject: [PATCH] =?UTF-8?q?New=20lemma=20`Next=5Funinj=20x=20:=20=E2=88=83?=
 =?UTF-8?q?=20a,=20x=20=E2=89=A1=20Next=20a`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This lemma allows one to get the witness out of a later, without having
to use `later_car`, i.e. in a way that works in the on-paper version of
the logic.
---
 theories/algebra/ofe.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index fb39bc55a..716350954 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1022,6 +1022,8 @@ Section later.
   Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
   Proof. by intros x y. Qed.
 
+  Lemma Next_uninj x : ∃ a, x ≡ Next a.
+  Proof. by exists (later_car x). Qed.
   Instance later_car_anti_contractive n :
     Proper (dist n ==> dist_later n) later_car.
   Proof. move=> [x] [y] /= Hxy. done. Qed.
-- 
GitLab