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

Let x0 of type ι → ι be given.

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

Apply unknownprop_2ab88bc3cb73bc8bbab980b6b6fd9d920b44f54ff9f8140f78b2a17b00566385 with x0, λ x1 x2 . nat_p x2.

The subproof is completed by applying nat_0.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ nat_p (x1 x2)) ⟶ nat_p (Sigma_nat x0 x1).

Let x1 of type ι → ι be given.

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

Apply unknownprop_32bc7778cd02b216f957f8c5e9693c4b58b7ca04a4ca47b5f3adb522add7dd35 with x0, x1, λ x2 x3 . nat_p x3 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply add_nat_p with Sigma_nat x0 x1, x1 x0 leaving 2 subgoals.

Apply H1 with x1.

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 H2 with x0.

The subproof is completed by applying ordsuccI2 with x0.

■

Proofgold Proof