Let x0 of type ι be given.
Apply nat_ind with
λ x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ ordsucc x0) ⟶ Sigma_nat x1 (λ x3 . mul_nat (x2 x3) (exp_nat (ordsucc x0) x3)) ∈ exp_nat (ordsucc x0) x1 leaving 2 subgoals.
Let x1 of type ι → ι be given.
Assume H1:
∀ x2 . x2 ∈ 0 ⟶ x1 x2 ∈ ordsucc x0.
Apply unknownprop_2ab88bc3cb73bc8bbab980b6b6fd9d920b44f54ff9f8140f78b2a17b00566385 with
λ x2 . mul_nat (x1 x2) (exp_nat (ordsucc x0) x2),
λ x2 x3 . x3 ∈ exp_nat (ordsucc x0) 0.
Apply nat_primrec_0 with
1,
λ x2 x3 . mul_nat (ordsucc x0) x3,
λ x2 x3 . 0 ∈ x3.
The subproof is completed by applying In_0_1.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Apply unknownprop_32bc7778cd02b216f957f8c5e9693c4b58b7ca04a4ca47b5f3adb522add7dd35 with
x1,
λ x3 . mul_nat (x2 x3) (exp_nat (ordsucc x0) x3),
λ x3 x4 . x4 ∈ exp_nat (ordsucc x0) (ordsucc x1) leaving 2 subgoals.
The subproof is completed by applying H1.