From 40ddc78f8619e5bbb2a18006c2fabc0d5c718638 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Dec 2016 22:03:19 +0100
Subject: [PATCH] resurrect proof that later_car is 'anti-contractive'

---
 algebra/ofe.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/algebra/ofe.v b/algebra/ofe.v
index d979299f0..06ca77883 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -874,6 +874,10 @@ Section later.
   Lemma contractive_alt {B : ofeT} (f : A → B) :
     Contractive f ↔ (∀ n x y, Next x ≡{n}≡ Next y → f x ≡{n}≡ f y).
   Proof. done. Qed.
+
+  Lemma later_car_anti_contractive :
+    ∀ n, Proper (dist n ==> dist_later n) later_car.
+  Proof. move=> n [x] [y] /= Hxy. done. Qed.
 End later.
 
 Arguments laterC : clear implicits.
-- 
GitLab