The rewrite rules for monads are carefully chosen so that
functor_norm will not introduce monadic vocabulary in a context where
applicatives would do just fine but will handle monadic notation
already present in an expression.
In a context where monadic reasoning is desired
simp with monad_norm
will translate functor and applicative notation into monad notation
and use regular
functor_norm rules as well.
functor, applicative, monad, simp
reduce the equivalence between two state monads to the equivalence between their respective function spaces
reduce the equivalence between two reader monads to the equivalence between their respective function spaces