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_127a8016213772da1e30a83ff8e90fea4b16395e6bcc47f8f75e4e8554f11176 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 2 = x2.
The subproof is completed by applying unknownprop_59a8dad2c0ad2592e27b9b4d31015a92d572a4eb8cb90378d5ba685d69740110 with x0, x1, x2, x3, x4.