Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_ab640183089126bd192ea777bf3d0693f7fc019527e86171644bd6e54256c0e4 with
lam 2 (λ x4 . If_i (x4 = 0) x0 x1),
lam 2 (λ x4 . If_i (x4 = 0) x2 x3),
λ x4 x5 . ap x5 0 = x0.
The subproof is completed by applying unknownprop_ab640183089126bd192ea777bf3d0693f7fc019527e86171644bd6e54256c0e4 with x0, x1.