proposition: Lemma JOINE A : @JOIN A = Join \o M # (M # Join \o swap).
proof: Proof. rewrite /JOIN. rewrite natural. rewrite -(compA Join) FCompE. by rewrite -(@functor_o M). Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib