Let x0 of type ο be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_e2282b8dae7947407e5c6c7e4a640634b1680442965ca2c1e158d5a5fa02ea67 with
x0,
x1,
x2,
or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2) leaving 2 subgoals.
Assume H0: x0.
Assume H1:
If_i x0 x1 x2 = x1.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
If_i x0 x1 x2 = x1,
If_i x0 x1 x2 = x2.
The subproof is completed by applying H1.
Assume H1:
If_i x0 x1 x2 = x2.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
If_i x0 x1 x2 = x1,
If_i x0 x1 x2 = x2.
The subproof is completed by applying H1.