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.
Let x22 of type ι be given.
Let x23 of type ι be given.
Let x24 of type ι be given.
Apply unknownprop_47c5cf16495685edf785d0343abce46ff38093017768e66700ff51c835d43c02 with
lam 5 (λ x25 . If_i (x25 = 0) x0 (If_i (x25 = 1) x1 (If_i (x25 = 2) x2 (If_i (x25 = 3) x3 x4)))),
lam 5 (λ x25 . If_i (x25 = 0) x5 (If_i (x25 = 1) x6 (If_i (x25 = 2) x7 (If_i (x25 = 3) x8 x9)))),
lam 5 (λ x25 . If_i (x25 = 0) x10 (If_i (x25 = 1) x11 (If_i (x25 = 2) x12 (If_i (x25 = 3) x13 x14)))),
lam 5 (λ x25 . If_i (x25 = 0) x15 (If_i (x25 = 1) x16 (If_i (x25 = 2) x17 (If_i (x25 = 3) x18 x19)))),
lam 5 (λ x25 . If_i (x25 = 0) x20 (If_i (x25 = 1) x21 (If_i (x25 = 2) x22 (If_i (x25 = 3) x23 x24)))),
λ x25 x26 . ap x26 0 = x15.
The subproof is completed by applying unknownprop_127a8016213772da1e30a83ff8e90fea4b16395e6bcc47f8f75e4e8554f11176 with x15, x16, x17, x18, x19.