Let x0 of type ι be given.
Apply SNo_eps_ with
x0.
The subproof is completed by applying H0.
Apply nat_ind with
λ x1 . mul_SNo (eps_ x0) x1 ∈ SNoS_ omega leaving 2 subgoals.
Apply mul_SNo_zeroR with
eps_ x0,
λ x1 x2 . x2 ∈ SNoS_ omega leaving 2 subgoals.
The subproof is completed by applying L1.
Apply omega_SNoS_omega with
0.
Apply nat_p_omega with
0.
The subproof is completed by applying nat_0.
Let x1 of type ι be given.
Apply add_SNo_1_ordsucc with
x1,
λ x2 x3 . mul_SNo (eps_ x0) x2 ∈ SNoS_ omega leaving 2 subgoals.
Apply nat_p_omega with
x1.
The subproof is completed by applying H2.
Apply mul_SNo_distrL with
eps_ x0,
x1,
1,
λ x2 x3 . x3 ∈ SNoS_ omega leaving 4 subgoals.
The subproof is completed by applying L1.
Apply omega_SNo with
x1.
Apply nat_p_omega with
x1.
The subproof is completed by applying H2.
Apply omega_SNo with
1.
Apply nat_p_omega with
1.
The subproof is completed by applying nat_1.
Apply mul_SNo_oneR with
eps_ x0,
λ x2 x3 . add_SNo (mul_SNo (eps_ x0) x1) x3 ∈ SNoS_ omega leaving 2 subgoals.
The subproof is completed by applying L1.
Apply add_SNo_SNoS_omega with
mul_SNo (eps_ x0) x1,
eps_ x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply SNo_eps_SNoS_omega with
x0.
The subproof is completed by applying H0.