proposition: Lemma prod1 : Prod.prod1 (@prod).
proof: Proof. move=> A B f; rewrite {1}/prod. rewrite -[LHS]compA Hswap1 (compA (M # Join)) -functor_o. by rewrite -natural functor_o -compA. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib