Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with
λ x0 . minus_SNo x0 ∈ int_alt1 leaving 2 subgoals.
Let x0 of type ι be given.
Apply unknownprop_a66fb27a7b2af57722c6537d3983b55a12cc28475f1d8b8d9bdb1d857010e7af with
x0.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Apply minus_SNo_invol with
x0,
λ x1 x2 . x2 ∈ int_alt1 leaving 2 subgoals.
Apply ordinal_SNo with
x0.
Apply nat_p_ordinal with
x0.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with
x0.
The subproof is completed by applying H0.