proposition: Lemma bind_fmap (A B C : UU0) (f : A -> B) (m : M A) (g : B -> M C) : fmap f m >>= g = m >>= (g \o f).
proof: Proof. by rewrite fmapE bindA; under eq_bind do rewrite bindretf. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)