From bbd381206a4b0d25d597762f9b0adb8563021069 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 25 Oct 2019 22:01:29 +0200
Subject: [PATCH] Add `later_map_proper`.

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

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index e8b300267..f9c7de6c2 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1081,6 +1081,10 @@ Instance later_map_ne {A B : ofeT} (f : A → B) n :
   Proper (dist (pred n) ==> dist (pred n)) f →
   Proper (dist n ==> dist n) (later_map f) | 0.
 Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
+Instance later_map_proper {A B : ofeT} (f : A → B) :
+  Proper ((≡) ==> (≡)) f →
+  Proper ((≡) ==> (≡)) (later_map f).
+Proof. solve_proper. Qed.
 Lemma later_map_id {A} (x : later A) : later_map id x = x.
 Proof. by destruct x. Qed.
 Lemma later_map_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
-- 
GitLab