proposition: Lemma JOIN_ret : JoinLaws.left_unit (CRet M N) (@JOIN').
proof: Proof. move=> A; rewrite /JOIN'. rewrite /=. rewrite /CRet. rewrite compA. rewrite -(compA Join (M # prod) Ret) (natural ret). by rewrite [LHS]compA (compA Join) joinretM compidf Hprod2. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib