Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply ordinal_Hered with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_20efab00e3dc5c8e2d82b77f53b1908d677eb3dc4b30a4906cc4d47b903d7af9 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_20efab00e3dc5c8e2d82b77f53b1908d677eb3dc4b30a4906cc4d47b903d7af9 with
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H1.
Apply unknownprop_035a7a7a8429e679b3938433bc18b326c1c9da99a6b1758a95f16843b008d68d with
bc82c.. x2 x1,
bc82c.. x0 x1 leaving 3 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L4.
Apply unknownprop_b751afd4b96b439a72771c5e6447c46f37e6851a11a9a372baaf45b11a370b67 with
x2,
x1,
x0 leaving 4 subgoals.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x2.
The subproof is completed by applying L3.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_397dcfaa62ddf41d498e7fd580ff4a854ed9ebd3c9ab727b2b23fe272ecb1aa4 with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.