Let x0 of type ι be given.
Claim L1:
∀ x2 : ι → ο . x2 y1 ⟶ x2 (add_CSNo x0 1)Let x2 of type ι → ο be given.
Apply add_SNo_add_CSNo with
y1,
1,
λ x3 x4 . (λ x5 . x2) x4 x3 leaving 3 subgoals.
Apply omega_SNo with
y1.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Apply add_SNo_1_ordsucc with
y1,
λ x3 . x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x2 of type ι → ι → ο be given.
Apply L1 with
λ x3 . x2 x3 y1 ⟶ x2 y1 x3.
Assume H2: x2 y1 y1.
The subproof is completed by applying H2.