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 1 = x3.
The subproof is completed by applying unknownprop_c08558c9c7b6c1be6215b272fb7932c68e2862a19045743bcd34753544c4d493 with x2, x3.