proposition: Lemma monad_morphism_natural : forall A B f m, f <$> (θ A m) = θ B (f <$> m).
proof: Proof. intros. cbv. rewrite mon_morph_bind. cbv ; f_equal. extensionality a. rewrite mon_morph_ret ; reflexivity. Qed.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)