Let x0 of type ι be given.
Let x1 of type ι be given.
Apply ordinal_Hered with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x1.
The subproof is completed by applying L2.
Apply unknownprop_b0d5c07b58c35dec2d98b8c0aef5865d54317627a7a2b363b61462669e811c57 with
x1.
The subproof is completed by applying L2.
Apply unknownprop_6987e7564cf46ad4d313ff96c864cc87566281cc7f9f5613cde1c6af34a43fdb with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply L4 with
λ x2 x3 . prim1 x3 x0.
The subproof is completed by applying H1.