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.
Assume H0:
In (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)) (Sep2 x0 x1 x2).
Apply unknownprop_c017a644eb6411fee34aba2858ad95d7edc6f065e01505f0c19557e300a42f32 with
x0,
x1,
x2,
x3,
x4,
In x4 (x1 x3) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2:
In x4 (x1 x3).
Assume H3: x2 x3 x4.
The subproof is completed by applying H2.