diff --git a/src/libraries/monads/monad.mli b/src/libraries/monads/monad.mli
index e3f89ca85d66f531cd38b419e1d823012e6c881e..849265e1cc83035fb6828086b275854ec1db88f6 100644
--- a/src/libraries/monads/monad.mli
+++ b/src/libraries/monads/monad.mli
@@ -167,7 +167,7 @@ end
 
     1. ∀x:'a, ∀f:('a -> 'b), [return (f x) ≣ map f (return x)]
 
-    2. ∀m:('a t t t), [map flatten (flatten m) ≣ flatten (flatten m)]
+    2. ∀m:('a t t t), [flatten (map flatten m) ≣ flatten (flatten m)]
 
     3. ∀m:('a t), [flatten (map return m) ≣ flatten (return m) ≣ m]