Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_4db127623a54dea607d4178c4cffe8099fa715d4dd5c11459d1bd4ea367db087 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_4db127623a54dea607d4178c4cffe8099fa715d4dd5c11459d1bd4ea367db087 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_497ef0b809178e9ac674acf0f41f994a7e76b824de0430efd934f6540a71daab with
x0,
x1,
x0 = x1 leaving 5 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply FalseE with
x0 = x1.
Apply unknownprop_b5d0a0123c3a8bc9dcc2915dc24ee4bb0a510635f6946e2a5486e14fe0d606b6 with
x1,
x0.
Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with
x0,
x1.
The subproof is completed by applying H2.
Apply unknownprop_6b8c05b4706c6a2c02124e3308f200f9e07b70239cb1fbcf7704eccbd6800c20 with
x1,
x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
The subproof is completed by applying L6.
Assume H5: x0 = x1.
The subproof is completed by applying H5.
Apply FalseE with
x0 = x1.
Apply unknownprop_b5d0a0123c3a8bc9dcc2915dc24ee4bb0a510635f6946e2a5486e14fe0d606b6 with
x0,
x1.
The subproof is completed by applying H2.
Apply unknownprop_6b8c05b4706c6a2c02124e3308f200f9e07b70239cb1fbcf7704eccbd6800c20 with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying L6.