Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Assume H0: ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x0 x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 = x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19.
Apply functional extensionality with
x0 x1,
x2.
Let x3 of type ι be given.
Apply functional extensionality with
x0 x1 x3,
x2 x3.
Let x4 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4,
x2 x3 x4.
Let x5 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5,
x2 x3 x4 x5.
Let x6 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6,
x2 x3 x4 x5 x6.
Let x7 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7,
x2 x3 x4 x5 x6 x7.
Let x8 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7 x8,
x2 x3 x4 x5 x6 x7 x8.
Let x9 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7 x8 x9,
x2 x3 x4 x5 x6 x7 x8 x9.
Let x10 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7 x8 x9 x10,
x2 x3 x4 x5 x6 x7 x8 x9 x10.
Let x11 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7 x8 x9 x10 x11,
x2 x3 x4 x5 x6 x7 x8 x9 x10 x11.
Let x12 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12,
x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12.
Let x13 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13,
x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13.
Let x14 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14,
x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14.
Let x15 of type ι be given.
Apply functional extensionality with
x0 x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ...,
....