Let x0 of type ι → ο be given.
Let x1 of type ι → ι → ι → ο be given.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι → ι → ι → ι → ι be given.
Let x4 of type ι → ι be given.
Let x5 of type ι → ι → ι → ι be given.
Let x6 of type ι → ι be given.
Let x7 of type ι → ι be given.
The subproof is completed by applying and3E with
MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x8 . x8) (λ x8 x9 x10 . x10) x4 x5 x6,
MetaNatTrans_strict x0 x1 x2 x3 x0 x1 x2 x3 (λ x8 . x4 (x4 x8)) (λ x8 x9 x10 . x5 (x4 x8) (x4 x9) (x5 x8 x9 x10)) x4 x5 x7,
MetaMonad x0 x1 x2 x3 x4 x5 x6 x7.