From 1fbbd48ca4a9237ac697403ace447cf556ec37fd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Jan 2016 18:19:57 +0100
Subject: [PATCH] More about later.

---
 modures/cofe.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/modures/cofe.v b/modures/cofe.v
index 5f1e2a4c3..1b8913b96 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -334,6 +334,8 @@ Section later.
   Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
   Global Instance Later_contractive : Contractive (@Later A).
   Proof. by intros n ??. Qed.
+  Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Later A).
+  Proof. by intros x y. Qed.
 End later.
 
 Arguments laterC : clear implicits.
-- 
GitLab