Search for blocks/addresses/...

Proofgold Proof

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