proposition: Lemma JOIN_naturality : @naturality _ _ (JOIN).
proof: Proof. by move=> ?? g; rewrite JOINE -/prod (Prod.JOIN_naturality prod1 g) JOINE. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib