proposition: Lemma prod3 : Prod.prod3 (@prod).
proof: Proof. move=> A; rewrite /prod /CRet. rewrite (@functor_o N) (compA (M # Join \o swap)) -(compA (_ # Join)) Hswap3. by rewrite (natural ret) -[LHS]compA joinMret compfid. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib