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.
Apply unknownprop_b9f4ecece16a3f4b44463b508cc3b9f5d1731684163a4bbdbf54ad9580b00fef with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x12,
x13,
MetaFunctor_strict 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 H4:
MetaFunctor x0 x1 x2 x3 x4 x5 x6 x7 x12 x13.
Apply unknownprop_b9f4ecece16a3f4b44463b508cc3b9f5d1731684163a4bbdbf54ad9580b00fef with
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x14,
x15,
MetaFunctor_strict 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 H7:
MetaFunctor x4 x5 x6 x7 x8 x9 x10 x11 x14 x15.
Apply unknownprop_3d05796578cdc17ebd2096167db48ecef934256d250d1637eb5dd67225cdfe05 with
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 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Apply unknownprop_8302545817abf61efcb2e2df201448c4fe3749289f4085fcd63d304083a57977 with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12,
x13,
x14,
x15 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H7.