Apply functional extensionality with
55574.. u20,
λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 . x20.
Let x0 of type ι be given.
Apply functional extensionality with
55574.. u20 x0,
(λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x21) x0.
Let x1 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1,
(λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x22) x0 x1.
Let x2 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2,
(λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x23) x0 x1 x2.
Let x3 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3,
(λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x24) x0 x1 x2 x3.
Let x4 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4,
(λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 . x25) x0 x1 x2 x3 x4.
Let x5 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5,
(λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 . x26) x0 x1 x2 x3 x4 x5.
Let x6 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5 x6,
(λ x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 . x27) x0 x1 x2 x3 x4 x5 x6.
Let x7 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5 x6 x7,
(λ x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 . x28) x0 x1 x2 x3 x4 x5 x6 x7.
Let x8 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5 x6 x7 x8,
(λ x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 . x29) x0 x1 x2 x3 x4 x5 x6 x7 x8.
Let x9 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
(λ x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 . x30) x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
Let x10 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10,
(λ x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x31) x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10.
Let x11 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11,
(λ x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 . x32) x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11.
Let x12 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12,
(λ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 . x33) x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12.
Let x13 of type ι be given.
Apply functional extensionality with
55574.. u20 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 ... ... ... ...,
....