proposition: Lemma bindmeta : BindLaws.right_neutral (bind eps) eta.
proof: Proof. rewrite /BindLaws.right_neutral => A m. rewrite /bind /mu -(compE (g # _)). by rewrite -functor_o AdjointFunctor.tri_left functor_id. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy