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