Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H0:
lam 2 (λ x4 . If_i (x4 = 0) x0 x1) = lam 2 (λ x4 . If_i (x4 = 0) x2 x3).
Apply andE with
x0 = x2,
x1 = x3.
Apply unknownprop_77651e64f1d2b5ae61aed7a8d53760794c482632a5582c8b02b82711d0ded9f2 with
x0,
x1,
x2,
x3.
The subproof is completed by applying H0.