proposition: Lemma bind_left_neutral_hom_fun (r : forall A, {hom A, M A}) : BindLaws.left_neutral b r <-> forall A B (f : {hom A, M B}), b f \o r A = f.
proof: Proof. by split; move=> H A B f; move: (H A B f); move/hom_ext. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)