Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Claim L5: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4
Let x6 of type ι → ο be given.
set y7 to be λ x7 . x6
Apply mul_SNo_assoc with
x2,
x3,
mul_SNo y4 y5,
λ x8 x9 . y7 x9 x8 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply SNo_mul_SNo with
y4,
y5 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Claim L6: ∀ x10 : ι → ο . x10 y9 ⟶ x10 y8
Let x10 of type ι → ο be given.
set y11 to be λ x11 . x10
Apply mul_SNo_assoc with
x6,
y7,
y8,
λ x12 x13 . x13 = mul_SNo y7 (mul_SNo x6 y8),
λ x12 x13 . y11 (mul_SNo y5 x12) (mul_SNo y5 x13) leaving 5 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply mul_SNo_assoc with
y7,
x6,
y8,
λ x12 x13 . mul_SNo (mul_SNo x6 y7) y8 = x13 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Claim L7: ∀ x14 : ι → ο . x14 y13 ⟶ x14 y12
Let x14 of type ι → ο be given.
set y15 to be λ x15 . x14
Apply mul_SNo_com with
y8,
y9,
λ x16 x17 . y15 (mul_SNo x16 x10) (mul_SNo x17 x10) leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
Let x14 of type ι → ι → ο be given.
Apply L7 with
λ x15 . x14 x15 y13 ⟶ x14 y13 x15.
Assume H8: x14 y13 y13.
The subproof is completed by applying H8.
The subproof is completed by applying H6.
set y10 to be λ x10 . y9
Apply L6 with
λ x11 . y10 x11 y9 ⟶ y10 y9 x11 leaving 2 subgoals.
Assume H7: y10 y9 y9.
The subproof is completed by applying H7.
Apply mul_SNo_assoc with
x6,
y8,
mul_SNo y7 y9,
λ x11 . y10 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply SNo_mul_SNo with
y7,
y9 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying L6.
Let x6 of type ι → ι → ο be given.
Apply L5 with
λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H6: x6 y5 y5.
The subproof is completed by applying H6.
Apply unknownprop_891bd8eaccd4934854a1a39a96fa375f8b43c939234e5ead477578dfa15afa04 with
SNo,
add_SNo,
mul_SNo,
λ x0 . mul_SNo x0 x0,
minus_SNo leaving 15 subgoals.
The subproof is completed by applying SNo_add_SNo.
The subproof is completed by applying SNo_mul_SNo.
The subproof is completed by applying add_SNo_com_3_0_1.
The subproof is completed by applying L0.
The subproof is completed by applying mul_SNo_distrL.
The subproof is completed by applying mul_SNo_distrR.
Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying H3.
The subproof is completed by applying SNo_minus_SNo.
The subproof is completed by applying minus_SNo_invol.
The subproof is completed by applying add_SNo_minus_L2.
The subproof is completed by applying add_SNo_minus_SNo_prop2.
The subproof is completed by applying mul_SNo_minus_distrL.
The subproof is completed by applying mul_SNo_minus_distrR.
The subproof is completed by applying mul_SNo_com.
The subproof is completed by applying L1.