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_36e12e654911209cf6139dcce25eccbb5fde1b810c75c2e7ca0621b0951e30f5 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 3 = x3.
The subproof is completed by applying unknownprop_23cea816b4176293b3d8ba4787692b8cb93e0a3eae6b638b0967d563a0bdc507 with x0, x1, x2, x3.