proposition: Lemma dorp4 : Dorp.dorp4 (@dorp).
proof: Proof. move=> A; rewrite {1}/dorp {1}/Dorp.JOIN -JOIN_dorp JOIN_prod. rewrite (compA (Join \o M # swap)) -(compA Join). rewrite (natural join). rewrite (compA Join Join) -joinA. rewrite -2![LHS]compA FCompE. rewrite -(@functor_o M) -(@functor_o M). rewrite (compA Join (M # swap) prod) -/dorp -Hswap4 functor_o. by rewrite [LHS]compA -JOINE JOIN_dorp. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib