proposition: Lemma fmap_oE (M : functor) (A B C : UU0) (f : A -> B) (g : C -> A) (m : M C) : (M # (f \o g)) m = (M # f) ((M # g) m).
proof: Proof. by rewrite functor_o. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy