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.
Apply unknownprop_8a884b2bd6ff36eba8856072c2baa52cff32d5e85b68403b704927d5d62d4773 with
lam 3 (λ x9 . If_i (x9 = 0) x0 (If_i (x9 = 1) x1 x2)),
lam 3 (λ x9 . If_i (x9 = 0) x3 (If_i (x9 = 1) x4 x5)),
lam 3 (λ x9 . If_i (x9 = 0) x6 (If_i (x9 = 1) x7 x8)),
λ x9 x10 . ap x10 2 = x8.
The subproof is completed by applying unknownprop_8a884b2bd6ff36eba8856072c2baa52cff32d5e85b68403b704927d5d62d4773 with x6, x7, x8.