Let x0 of type ι be given.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
0 = ordsucc x0.
Apply H0 with
λ x1 x2 . In x0 x1 ⟶ False.
The subproof is completed by applying unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x0.
Apply L1.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x0.