Apply add_nat_add_SNo with
4,
3,
λ x0 x1 . x0 = 7 leaving 3 subgoals.
Apply nat_p_omega with
4.
The subproof is completed by applying nat_4.
Apply nat_p_omega with
3.
The subproof is completed by applying nat_3.
Apply add_nat_SR with
4,
2,
λ x0 x1 . x1 = 7 leaving 2 subgoals.
The subproof is completed by applying nat_2.
set y1 to be 7
Claim L0: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0
Let x2 of type ι → ο be given.
Assume H0: x2 7.
set y3 to be λ x3 . x2
Apply add_nat_SR with
4,
1,
λ x4 x5 . x5 = 6,
λ x4 x5 . y3 (ordsucc x4) (ordsucc x5) leaving 3 subgoals.
The subproof is completed by applying nat_1.
set y5 to be 6
Claim L1: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4
Let x6 of type ι → ο be given.
Assume H1: x6 6.
set y7 to be λ x7 . x6
Apply add_nat_SR with
4,
0,
λ x8 x9 . x9 = 5,
λ x8 x9 . y7 (ordsucc x8) (ordsucc x9) leaving 3 subgoals.
The subproof is completed by applying nat_0.
set y9 to be 5
Claim L2: ∀ x10 : ι → ο . x10 y9 ⟶ x10 y8
Let x10 of type ι → ο be given.
Assume H2: x10 5.
set y11 to be λ x11 . x10
Apply add_nat_0R with
4,
λ x12 x13 . y11 (ordsucc x12) (ordsucc x13).
The subproof is completed by applying H2.
Let x10 of type ι → ι → ο be given.
Apply L2 with
λ x11 . x10 x11 y9 ⟶ x10 y9 x11.
Assume H3: x10 y9 y9.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
Let x6 of type ι → ι → ο be given.
Apply L1 with
λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H2: x6 y5 y5.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
Let x2 of type ι → ι → ο be given.
Apply L0 with
λ x3 . x2 x3 y1 ⟶ x2 y1 x3.
Assume H1: x2 y1 y1.
The subproof is completed by applying H1.