Apply nat_ind with λ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ nat_p (x1 x2)) ⟶ nat_p (nat_primrec 1 (λ x2 x3 . mul_nat (x1 x2) x3) x0) leaving 2 subgoals.

Let x0 of type ι → ι be given.

Assume H0: ∀ x1 . x1 ∈ 0 ⟶ nat_p (x0 x1).

Apply nat_primrec_0 with 1, λ x1 x2 . mul_nat (x0 x1) x2, λ x1 x2 . nat_p x2.

The subproof is completed by applying nat_1.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ nat_p (x1 x2)) ⟶ nat_p (nat_primrec 1 (λ x2 x3 . mul_nat (x1 x2) x3) x0).

Let x1 of type ι → ι be given.

Assume H2: ∀ x2 . x2 ∈ ordsucc x0 ⟶ nat_p (x1 x2).

Claim L3: ∀ x2 . x2 ∈ x0 ⟶ nat_p (x1 x2)

Let x2 of type ι be given.

Assume H3: x2 ∈ x0.

Apply H2 with x2.

Apply ordsuccI1 with x0, x2.

The subproof is completed by applying H3.

Apply nat_primrec_S with 1, λ x2 x3 . mul_nat (x1 x2) x3, x0, λ x2 x3 . nat_p x3 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply mul_nat_p with x1 x0, nat_primrec 1 (λ x2 x3 . mul_nat (x1 x2) x3) x0 leaving 2 subgoals.

Apply H2 with x0.

The subproof is completed by applying ordsuccI2 with x0.

Apply H1 with λ x2 . x1 x2.

The subproof is completed by applying L3.

■

Proofgold Proof