Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Claim L3: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Claim L4: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
set y9 to be λ x9 . x8
Apply add_CSNo_com with
x5,
y6,
λ x10 x11 . y9 (add_CSNo y4 x10) (add_CSNo y4 x11) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
set y8 to be λ x8 . y7
Apply L4 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H5: y8 y7 y7.
The subproof is completed by applying H5.
set y9 to be λ x9 . y8
Apply add_CSNo_assoc with
x5,
y7,
y6,
λ x10 x11 . y9 x11 x10 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
Claim L5: ∀ x12 : ι → ο . x12 y11 ⟶ x12 y10
Let x12 of type ι → ο be given.
set y13 to be λ x13 . x12
Apply add_CSNo_com with
y8,
y10,
λ x14 x15 . y13 (add_CSNo x14 y9) (add_CSNo x15 y9) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
set y12 to be λ x12 . y11
Apply L5 with
λ x13 . y12 x13 y11 ⟶ y12 y11 x13 leaving 2 subgoals.
Assume H6: y12 y11 y11.
The subproof is completed by applying H6.
Apply add_CSNo_assoc with
y11,
y9,
y10,
λ x13 . y12 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying L5.
Let x5 of type ι → ι → ο be given.
Apply L3 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H4: x5 y4 y4.
The subproof is completed by applying H4.