Let x0 of type ι be given.
Apply H0 with
even_nat (ordsucc (ordsucc x0)).
Apply H2 with
even_nat (ordsucc (ordsucc x0)).
Let x1 of type ι be given.
Apply H3 with
even_nat (ordsucc (ordsucc x0)).
Apply andI with
ordsucc (ordsucc x0) ∈ omega,
∃ x2 . and (x2 ∈ omega) (ordsucc (ordsucc x0) = mul_nat 2 x2) leaving 2 subgoals.
Apply omega_ordsucc with
ordsucc x0.
Apply omega_ordsucc with
x0.
The subproof is completed by applying H1.
Let x2 of type ο be given.
Apply H6 with
ordsucc x1.
Apply andI with
ordsucc x1 ∈ omega,
ordsucc (ordsucc x0) = mul_nat 2 (ordsucc x1) leaving 2 subgoals.
Apply omega_ordsucc with
x1.
The subproof is completed by applying H4.
Apply mul_nat_SR with
2,
x1,
λ x3 x4 . ordsucc (ordsucc x0) = x4 leaving 2 subgoals.
Apply omega_nat_p with
x1.
The subproof is completed by applying H4.
Apply H5 with
λ x3 x4 . ordsucc (ordsucc x0) = add_nat 2 x3.
Apply add_nat_SL with
1,
x0,
λ x3 x4 . ordsucc (ordsucc x0) = x4 leaving 3 subgoals.
The subproof is completed by applying nat_1.
Apply omega_nat_p with
x0.
The subproof is completed by applying H1.
Claim L7: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
set y6 to be λ x6 . x5
Apply add_nat_SL with
0,
x2,
λ x7 x8 . ordsucc x2 = x8,
λ x7 x8 . y6 (ordsucc x7) (ordsucc x8) leaving 4 subgoals.
The subproof is completed by applying nat_0.
Apply omega_nat_p with
x2.
The subproof is completed by applying H1.
Claim L8: ∀ x9 : ι → ο . x9 y8 ⟶ x9 y7
Let x9 of type ι → ο be given.
set y10 to be λ x10 . x9
Apply add_nat_0L with
y4,
λ x12 x13 . y11 x13 x12 leaving 2 subgoals.
Apply omega_nat_p with
y4.
The subproof is completed by applying H1.
The subproof is completed by applying H8.
Let x9 of type ι → ι → ο be given.
Apply L8 with
λ x10 . x9 x10 y8 ⟶ x9 y8 x10.
Assume H9: x9 y8 y8.
The subproof is completed by applying H9.
The subproof is completed by applying H7.
Let x5 of type ι → ι → ο be given.
Apply L7 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H8: x5 y4 y4.
The subproof is completed by applying H8.