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