proposition: Lemma JOIN_fmap_ret : JoinLaws.right_unit (@CRet M N) (@JOIN').
proof: Proof. move=> A; rewrite /JOIN /CRet. rewrite -(compA (M # Join) dorp). rewrite (@functor_o [the functor of M \o N]). rewrite (compA dorp) Hdorp3. rewrite compidf -functor_o. by rewrite joinMret functor_id. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib