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