proposition: Lemma muMA A : @mu A \o @mu (M A) = @mu A \o (M # @mu A).
proof: Proof. have -> : g # eps (f A) \o g # eps (f (M A)) = g # (@eps (f A) \o @eps (f (M A))) by rewrite functor_o. by rewrite epsC functor_o. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy