From 9ffa68a45ac7e5a5e707ba30ccd645fbb13e94e4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jan 2016 17:24:14 +0100
Subject: [PATCH] Eta lemma for later.
---
modures/cofe.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/modures/cofe.v b/modures/cofe.v
index f8d32d84a..b0b2de194 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -311,6 +311,8 @@ Inductive later (A : Type) : Type := Later { later_car : A }.
Add Printing Constructor later.
Arguments Later {_} _.
Arguments later_car {_} _.
+Lemma later_eta {A} (x : later A) : Later (later_car x) = x.
+Proof. by destruct x. Qed.
Section later.
Context {A : cofeT}.
--
GitLab