diff --git a/modures/cofe.v b/modures/cofe.v
index f8d32d84a5a409263aacf6a1d89b65f5a9c738db..b0b2de1944d7ecbd00507999da15df55d8dd316a 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}.