diff --git a/algebra/cofe.v b/algebra/cofe.v
index 193e2103caf67227cbb4306933560b3666319b6e..826db73562ec90fe213ce57cf59d628019473621 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -216,6 +216,10 @@ Arguments CofeMor {_ _} _ {_}.
 Add Printing Constructor cofeMor.
 Existing Instance cofe_mor_ne.
 
+Notation "'λne' x .. y , t" :=
+  (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _)
+  (at level 200, x binder, y binder, right associativity).
+
 Section cofe_mor.
   Context {A B : cofeT}.
   Global Instance cofe_mor_proper (f : cofeMor A B) : Proper ((≡) ==> (≡)) f.