proposition: Lemma joinMret : hierarchy.JoinLaws.right_unit ret join.
proof: Proof. by move=> a; rewrite joinE retE actmE (@category.joinMret _ M). Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures) hierarchy