Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
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 ordinal_Hered with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x2.
The subproof is completed by applying L5.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x0,
x2,
λ x3 x4 . prim1 x4 (bc82c.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L6.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x0,
x1,
λ x3 x4 . prim1 (bc82c.. x2 x0) x4 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply unknownprop_f118e9b0ed15e0baf93f78111ae4cc512c29fc0c894f179730bd322e9cda648d with
x1,
x0,
x2 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.