Let x0 of type ι be given.
Apply unknownprop_5e2628df9f5f85e18b5435fd3c0ad09162064b9312de3fdc10d248bc12486c0b with
ordsucc (ordsucc (ordsucc (ordsucc x0))).
Apply unknownprop_5e2628df9f5f85e18b5435fd3c0ad09162064b9312de3fdc10d248bc12486c0b with
x0.
The subproof is completed by applying H0.