Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply unknownprop_08307bdbb7a97185122351ee4a5953158d8e3481a107df1f643fe83793e0fbe1 with
x0,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Apply H3 with
x2.
Apply ordinal_Hered with
x0,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply unknownprop_eb2dfcc61b297e9bd5334705d22ba206e3441f9f0cfc821c0488b814ec57c600 with
x3,
x1 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H5.
Apply unknownprop_2c27682abc32e1c8a2160a07043a81afe1f256df4f0472edf3cf11efdcea8609 with
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply unknownprop_34004d936e9c770d7776a68f4fd89de16dd752c63a364055547f1f2fd867c6b6 with
x3,
x1 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying H5.
Apply L10 with
λ x4 x5 . prim1 x5 x0.
The subproof is completed by applying H4.
Apply H2 leaving 4 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying H8.
The subproof is completed by applying L7.
The subproof is completed by applying H9.