Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_74e6ddb76e51f556d0e4a910f649c4782bc9cb375d38baef38a8c05a47e8ef22 with
Power (Power 0),
λ x3 . If_i (In 0 x3) x1 x2,
x0,
or (x0 = x1) (x0 = x2) leaving 2 subgoals.
Apply unknownprop_cbe03b1d73461065a9cab3cfe58a3146c30e691f6f669990a6f43a4ec94a2bbe with
λ x3 x4 : ι → ι → ι . In x0 (x3 x1 x2).
The subproof is completed by applying H0.
Let x3 of type ι be given.
Claim L2:
x0 = If_i (In 0 x3) x1 x2Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with
In x3 (Power (Power 0)),
x0 = If_i (In 0 x3) x1 x2.
The subproof is completed by applying H1.
Apply unknownprop_e2282b8dae7947407e5c6c7e4a640634b1680442965ca2c1e158d5a5fa02ea67 with
In 0 x3,
x1,
x2,
or (x0 = x1) (x0 = x2) leaving 2 subgoals.
Assume H4:
If_i (In 0 x3) x1 x2 = x1.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
x0 = x1,
x0 = x2.
Apply H4 with
λ x4 x5 . x0 = x4.
The subproof is completed by applying L2.
Assume H3:
not (In 0 x3).
Assume H4:
If_i (In 0 x3) x1 x2 = x2.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
x0 = x1,
x0 = x2.
Apply H4 with
λ x4 x5 . x0 = x4.
The subproof is completed by applying L2.