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