proposition: Lemma bind_kleisli A B C m (f : A -> M B) (g : B -> M C) : m >>= (f >=> g) = (m >>= f) >>= g.
proof: Proof. by rewrite bindA; bind_ext => a; rewrite /kleisli !compE join_fmap. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)