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_72ee6a4729e4d36966f7c731b465de1ffff5565146924f50f9d4e56e3e4f5133 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 = x2.
The subproof is completed by applying unknownprop_8a884b2bd6ff36eba8856072c2baa52cff32d5e85b68403b704927d5d62d4773 with x0, x1, x2.