Let x0 of type ι be given.
Let x1 of type ι be given.
Apply ordinal_In_Or_Subq with
x0,
x1,
prim1 x0 x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply FalseE with
prim1 x0 x1.
Apply unknownprop_86d1ac064e08bd36bc8f8c7d3070ea65b389686b3ca603e510b47119b9d626ec with
x0.
Apply unknownprop_13b99fd000490b330591961fc1e419c9f4ce9013dd2d43edb6af3c0a8dc957a3 with
x0,
x1,
x0 leaving 5 subgoals.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_6b58ccf34c19b37f5faaafa5f54be6f18c6c4bc33a3c17e1c3faf38333ddc924 with
x1,
x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H3.