Let x0 of type ι be given.
Let x1 of type ι be given.
Apply ordinal_In_Or_Subq with
x1,
x0,
Subq x0 x1 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply FalseE with
Subq x0 x1.
Apply unknownprop_86d1ac064e08bd36bc8f8c7d3070ea65b389686b3ca603e510b47119b9d626ec with
x0.
Apply unknownprop_01059785170d3f6ee7ccae83a53df10446a7c0a3edc3b8aae06f45756a2928c3 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_397dcfaa62ddf41d498e7fd580ff4a854ed9ebd3c9ab727b2b23fe272ecb1aa4 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying H3.