Apply unknownprop_85336ee07ace71a942dc508d3b8c851d9d6bb88511443b7dafbf11b71c263f4d with
λ x0 . ordinal x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_d2696f7eb2bec05a6737b4f543c10fff1c0796b35a7b98004ed229df9dd391c9.
Let x0 of type ι be given.
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with
x0.
The subproof is completed by applying H1.