Let x0 of type ι be given.
Apply eps_ordsucc_half_add with
x0,
λ x1 x2 . SNoLt (eps_ (ordsucc x0)) x1 leaving 2 subgoals.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Apply add_SNo_eps_Lt with
eps_ (ordsucc x0),
ordsucc x0 leaving 2 subgoals.
Apply SNo_eps_ with
ordsucc x0.
Apply omega_ordsucc with
x0.
The subproof is completed by applying H0.
Apply omega_ordsucc with
x0.
The subproof is completed by applying H0.