proposition: Lemma VA' : F ~> [the functor of G \o (K \o J)] -> F ~> [the functor of G \o K \o J].
proof: Proof. move=> [s [] [GFs]]. apply: (@Nattrans.Pack F [the functor of (G \o K) \o J] _ (Nattrans.Class (isNatural.Axioms_ _ _ _))). exact: GFs. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib