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_c08558c9c7b6c1be6215b272fb7932c68e2862a19045743bcd34753544c4d493 with
lam 2 (λ x4 . If_i (x4 = 0) x0 x1),
lam 2 (λ x4 . If_i (x4 = 0) x2 x3),
λ x4 x5 . ap x5 0 = x2.
The subproof is completed by applying unknownprop_ab640183089126bd192ea777bf3d0693f7fc019527e86171644bd6e54256c0e4 with x2, x3.