Let x0 of type ι be given.
Apply unknownprop_833fce77b57f1904daf6dd60f4428eb41261613ee9bd44bd8c77191bee70a479 with
x0,
λ x1 x2 . ordinal x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with
x0.
The subproof is completed by applying H0.