Let x0 of type ο be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: x0.
Apply unknownprop_e2282b8dae7947407e5c6c7e4a640634b1680442965ca2c1e158d5a5fa02ea67 with
x0,
x1,
x2,
If_i x0 x1 x2 = x1 leaving 2 subgoals.
Assume H1: x0.
Assume H2:
If_i x0 x1 x2 = x1.
The subproof is completed by applying H2.
Apply FalseE with
If_i x0 x1 x2 = x2 ⟶ If_i x0 x1 x2 = x1.
Apply notE with
x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.