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:
not (If_i x0 x1 x2 = x3).
Apply unknownprop_e2282b8dae7947407e5c6c7e4a640634b1680442965ca2c1e158d5a5fa02ea67 with
x0,
x1,
x2,
False leaving 2 subgoals.
Assume H3: x0.
Assume H4:
If_i x0 x1 x2 = x1.
Apply H1 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply H4 with
λ x4 x5 . not (x4 = x3).
The subproof is completed by applying H0.
Assume H4:
If_i x0 x1 x2 = x2.
Apply H2 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply H4 with
λ x4 x5 . not (x4 = x3).
The subproof is completed by applying H0.