proposition: Lemma JOIN_fmap_ret : JoinLaws.right_unit (@CRet M N) (@JOIN').
proof: Proof. move=> A. rewrite /JOIN' /=. rewrite -compA. rewrite FCompE. rewrite -(@functor_o M). by rewrite Hprod3 joinMret. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib