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.
Let x19 of type ι be given.
Let x20 of type ι be given.
Let x21 of type ι be given.
Apply unknownprop_63c13366871d56b929a86e30fe3f917efdeb3d770effb105bd4d58ad234e36b2 with
x0,
u22,
λ x22 x23 . (λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x1 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x2 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x3 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x4 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x5 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x6 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x7 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x8 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x9 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x10 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x11 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x12 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x13 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x14 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x15 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x16 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x17 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x18 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x19 ((λ x24 x25 x26 x27 . If_i (x27 = x26) x24 x25) x20 x21 ((λ x24 : ι → ι . λ x25 . x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 x25))))))))))))))))))) ordsucc x22) x23) ((λ x24 : ι → ι . λ x25 . x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 x25)))))))))))))))))) ordsucc x22) x23) ((λ x24 : ι → ι . λ x25 . x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 x25))))))))))))))))) ordsucc x22) x23) ((λ x24 : ι → ι . λ x25 . x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 (x24 ...))))))))))))) ... ...) ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...) ... ...,
0,
...,
... leaving 2 subgoals.