Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H1:
x2 = x0 ⟶ False.
Assume H2:
x2 = x1 ⟶ False.
Apply unknownprop_75ddf832b1631756e4bbf96a65e15fca654982aa51c8799a97b68da7b8a2da12 with
x2,
x0,
x1,
False leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H3: x2 = x0.
Apply H1.
The subproof is completed by applying H3.
Assume H3: x2 = x1.
Apply H2.
The subproof is completed by applying H3.