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_cd1658f3a72c6a2bb94a2daab3e8270dc8dd343e6dd52f56f65d81dc131b0875 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 = x11.
The subproof is completed by applying unknownprop_23cea816b4176293b3d8ba4787692b8cb93e0a3eae6b638b0967d563a0bdc507 with x8, x9, x10, x11.