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

Let x0 of type ι → ι be given.

Assume H0: ∀ x1 . x1 ∈ 0 ⟶ x0 x1 ∈ setminus omega 1.

Apply nat_primrec_0 with 1, λ x1 x2 . mul_nat (x0 x1) x2, λ x1 x2 . x2 ∈ setminus omega 1.

Apply setminusI with omega, 1, 1 leaving 2 subgoals.

Apply nat_p_omega with 1.

The subproof is completed by applying nat_1.

The subproof is completed by applying In_irref with 1.

Let x0 of type ι be given.

Assume H0: nat_p x0.

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

Let x1 of type ι → ι be given.

Assume H2: ∀ x2 . x2 ∈ ordsucc x0 ⟶ x1 x2 ∈ setminus omega 1.

Claim L3: ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ setminus omega 1

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 . x3 ∈ setminus omega 1 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_87bf8388b36fffab96888ad3bd06efd3451825a154aa6df88807aa16f4771b8c 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