Let x0 of type ι be given.
Apply unknownprop_284dc111c6eb2bddb3c4d801652d8c8261bace09e41e64d83eb05adf646c0cc8 with
x0,
λ x1 x2 . x2 ∈ omega leaving 2 subgoals.
The subproof is completed by applying H0.
Apply omega_ordsucc with
x0.
The subproof is completed by applying H0.