proposition: Lemma fmapE (A B : UU0) (f : A -> B) (m : M A) : (M # f) m = m >>= (ret B \o f).
proof: Proof. by rewrite bindE [in RHS]functor_o -[in RHS]compE compA joinMret. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)