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_ad0347fd00c465af5dfdd914ea5ee88ed02126a7c7ef66823f6c720d34ff7b99 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 0 = x3.
The subproof is completed by applying unknownprop_72ee6a4729e4d36966f7c731b465de1ffff5565146924f50f9d4e56e3e4f5133 with x3, x4, x5.