Let x0 of type ι → ι be given.
Let x1 of type ι → ι be given.
Apply nat_ind with
λ x2 . (∀ x3 . x3 ∈ x2 ⟶ x0 x3 = x1 x3) ⟶ 05ecb.. x0 x2 = 05ecb.. x1 x2 leaving 2 subgoals.
Assume H0: ∀ x2 . x2 ∈ 0 ⟶ x0 x2 = x1 x2.
Apply unknownprop_89e7310d38716ec0d15b566dbd8df2f84011da8cd7b706cd43ff87121048033c with
x1,
λ x2 x3 . 05ecb.. x0 0 = x3.
The subproof is completed by applying unknownprop_89e7310d38716ec0d15b566dbd8df2f84011da8cd7b706cd43ff87121048033c with x0.
Let x2 of type ι be given.
Assume H1:
(∀ x3 . x3 ∈ x2 ⟶ x0 x3 = x1 x3) ⟶ 05ecb.. x0 x2 = 05ecb.. x1 x2.
Assume H2:
∀ x3 . x3 ∈ ordsucc x2 ⟶ x0 x3 = x1 x3.
Apply unknownprop_bfe386a724e0556e84046f452d416531498b4ec738b589b2f6a1e7f84e7dc85a with
x0,
x2,
λ x3 x4 . x4 = 05ecb.. x1 (ordsucc x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_bfe386a724e0556e84046f452d416531498b4ec738b589b2f6a1e7f84e7dc85a with
x1,
x2,
λ x3 x4 . mul_SNo (05ecb.. x0 x2) (x0 x2) = x4 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ι → ο be given.
Apply H1 with
λ x5 x6 . (λ x7 . x4) (mul_SNo x5 (x1 y3)) (mul_SNo x6 (x1 y3)) leaving 2 subgoals.
Let x5 of type ι be given.
Assume H4: x5 ∈ y3.
Apply H2 with
x5.
Apply ordsuccI1 with
y3,
x5.
The subproof is completed by applying H4.
Apply H2 with
y3,
λ x5 x6 . (λ x7 . x4) (mul_SNo (05ecb.. x2 y3) x5) (mul_SNo (05ecb.. x2 y3) x6) leaving 2 subgoals.
The subproof is completed by applying ordsuccI2 with y3.
The subproof is completed by applying H3.
Let x4 of type ι → ι → ο be given.
Apply L3 with
λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H4: x4 y3 y3.
The subproof is completed by applying H4.