Let x0 of type ι be given.
Let x1 of type ι be given.
Apply omega_ordsucc with
x0.
The subproof is completed by applying H0.
Apply SNo_eps_ with
x0.
The subproof is completed by applying H0.
Apply SNo_eps_ with
ordsucc x0.
The subproof is completed by applying L6.
Apply eps_ordsucc_Lt with
x0.
The subproof is completed by applying H0.
Apply SNoLeLt_tra with
add_SNo x1 (eps_ (ordsucc x0)),
eps_ (ordsucc x0),
eps_ x0 leaving 5 subgoals.
Apply SNo_add_SNo with
x1,
eps_ (ordsucc x0) leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying L8.
The subproof is completed by applying L8.
The subproof is completed by applying L7.
Apply add_SNo_0L with
eps_ (ordsucc x0),
λ x2 x3 . SNoLe (add_SNo x1 (eps_ (ordsucc x0))) x2 leaving 2 subgoals.
The subproof is completed by applying L8.
Apply add_SNo_Le1 with
x1,
eps_ (ordsucc x0),
0 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying L8.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H5.
The subproof is completed by applying L9.
Apply andI with
SNoLt (add_SNo x1 (eps_ (ordsucc x0))) (eps_ x0),
SNoLt (add_SNo (eps_ (ordsucc x0)) x1) (eps_ x0) leaving 2 subgoals.
The subproof is completed by applying L10.
Apply add_SNo_com with
eps_ (ordsucc x0),
x1,
λ x2 x3 . SNoLt x3 (eps_ x0) leaving 3 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying H2.
The subproof is completed by applying L10.