proposition: Lemma kleisliA A B C D (f : A -> M B) (g : B -> M C) (h : C -> M D) : f >=> g >=> h = f >=> (g >=> h).
proof: Proof. apply: funext_dep => a; rewrite !kleisliE bindA. by under [in RHS]eq_bind do rewrite kleisliE. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)