Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with
λ x0 . SNo x0 leaving 2 subgoals.
The subproof is completed by applying omega_SNo.
Let x0 of type ι be given.
Apply SNo_minus_SNo with
x0.
Apply omega_SNo with
x0.
The subproof is completed by applying H0.