Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
Sing 0,
1.
Let x0 of type ι be given.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
x0,
λ x1 x2 . In x0 (ordsucc x1) leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x0.