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.
Apply unknownprop_23cea816b4176293b3d8ba4787692b8cb93e0a3eae6b638b0967d563a0bdc507 with
lam 4 (λ x16 . If_i (x16 = 0) x0 (If_i (x16 = 1) x1 (If_i (x16 = 2) x2 x3))),
lam 4 (λ x16 . If_i (x16 = 0) x4 (If_i (x16 = 1) x5 (If_i (x16 = 2) x6 x7))),
lam 4 (λ x16 . If_i (x16 = 0) x8 (If_i (x16 = 1) x9 (If_i (x16 = 2) x10 x11))),
lam 4 (λ x16 . If_i (x16 = 0) x12 (If_i (x16 = 1) x13 (If_i (x16 = 2) x14 x15))),
λ x16 x17 . ap x17 1 = x13.
The subproof is completed by applying unknownprop_b4d9b28ffdfc26091f8308714bc32dda459f8ef72e65f6991a681b771ecda216 with x12, x13, x14, x15.