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.
Let x14 of type ι → ι be given.
Let x15 of type ι → ι → ι → ι be given.
Let x16 of type ι → ι be given.
Let x17 of type ι → ι → ι → ι be given.
Let x18 of type ι → ι be given.
Assume H0:
MetaNatTrans x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x18.
Assume H1:
MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x16 x17.
Apply unknownprop_60c5d36105bfcc8198cf1e849b691d909717c94b81b3fd20887e1f1d9372a027 with
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12,
x13,
x14,
x15,
x18,
MetaNatTrans x0 x1 x2 x3 x8 x9 x10 x11 (λ x19 . x12 (x16 x19)) (λ x19 x20 x21 . x13 (x16 x19) (x16 x20) (x17 x19 x20 x21)) (λ x19 . x14 (x16 x19)) (λ x19 x20 x21 . x15 (x16 x19) (x16 x20) (x17 x19 x20 x21)) (λ x19 . x18 (x16 x19)) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2: ∀ x19 . x4 x19 ⟶ x9 (x12 x19) (x14 x19) (x18 x19).
Assume H3: ∀ x19 x20 x21 . x4 x19 ⟶ x4 x20 ⟶ x5 x19 x20 x21 ⟶ x11 (x12 x19) (x14 x19) (x14 x20) (x15 x19 x20 x21) (x18 x19) = x11 (x12 x19) (x12 x20) (x14 x20) (x18 x20) (x13 x19 x20 x21).
Apply unknownprop_d4b40e23fc0295f5b3315cbc1d218fe48d2b71569cbf77e67c33e2487a1d9a24 with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x16,
x17,
MetaNatTrans x0 x1 x2 x3 x8 x9 x10 x11 (λ x19 . x12 (x16 x19)) (λ x19 x20 x21 . x13 (x16 x19) (x16 x20) (x17 x19 x20 x21)) (λ x19 . x14 (x16 x19)) (λ x19 x20 x21 . x15 (x16 x19) (x16 x20) (x17 x19 x20 x21)) (λ x19 . x18 (x16 x19)) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H4: ∀ x19 . x0 x19 ⟶ x4 (x16 x19).
Assume H5: ∀ x19 x20 x21 . x0 x19 ⟶ x0 x20 ⟶ x1 x19 x20 x21 ⟶ x5 (x16 x19) (x16 x20) (x17 x19 x20 x21).
Assume H6: ∀ x19 . x0 x19 ⟶ x17 x19 x19 (x2 x19) = x6 (x16 x19).
Assume H7: ∀ x19 x20 x21 x22 x23 . ... ⟶ x0 ... ⟶ x0 x21 ⟶ x1 x19 x20 x22 ⟶ x1 x20 x21 x23 ⟶ x17 x19 x21 (x3 x19 x20 x21 x23 x22) = x7 (x16 x19) (x16 x20) (x16 x21) (x17 x20 x21 x23) (x17 x19 x20 x22).