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.
Let x8 of type ι → ι be given.
Let x9 of type ι → ι → ι → ι be given.
Let x10 of type ι → ι be given.
Let x11 of type ι → ι → ι → ι be given.
Let x12 of type ι → ι be given.
Let x13 of type ι → ι be given.
The subproof is completed by applying and5E with
MetaFunctor_strict x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
MetaFunctor x4 x5 x6 x7 x0 x1 x2 x3 x10 x11,
MetaNatTrans x0 x1 x2 x3 x0 x1 x2 x3 (λ x14 . x14) (λ x14 x15 x16 . x16) (λ x14 . x10 (x8 x14)) (λ x14 x15 x16 . x11 (x8 x14) (x8 x15) (x9 x14 x15 x16)) x12,
MetaNatTrans x4 x5 x6 x7 x4 x5 x6 x7 (λ x14 . x8 (x10 x14)) (λ x14 x15 x16 . x9 (x10 x14) (x10 x15) (x11 x14 x15 x16)) (λ x14 . x14) (λ x14 x15 x16 . x16) x13,
MetaAdjunction x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13.