proposition: Lemma JOIN_ret : JoinLaws.left_unit (@CRet M N) (@JOIN').
proof: Proof. move=> A; rewrite /JOIN -[LHS]compA Hdorp2. rewrite -(@functor_o M). by rewrite joinretM functor_id. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib