Let x0 of type ι be given.

Assume H0: nat_p x0.

Let x1 of type ι → ο be given.

Assume H1: x1 0.

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

Apply nat_inv with x0, x1 x0 leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H3: x0 = 0.

Apply H3 with λ x2 x3 . x1 x3.

The subproof is completed by applying H1.

Assume H3: ∃ x2 . and (nat_p x2) (x0 = ordsucc x2).

Apply H3 with x1 x0.

Let x2 of type ι be given.

Assume H4: (λ x3 . and (nat_p x3) (x0 = ordsucc x3)) x2.

Apply H4 with x1 x0.

Assume H5: nat_p x2.

Assume H6: x0 = ordsucc x2.

Apply H6 with λ x3 x4 . x1 x4.

Apply H2 with ordsucc x2.

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

Apply nat_p_omega with ordsucc x2.

Apply nat_ordsucc with x2.

The subproof is completed by applying H5.

Assume H7: ordsucc x2 ∈ 1.

Apply neq_ordsucc_0 with x2.

Apply cases_1 with ordsucc x2, λ x3 . x3 = 0 leaving 2 subgoals.

The subproof is completed by applying H7.

Let x3 of type ι → ι → ο be given.

Assume H8: x3 0 0.

The subproof is completed by applying H8.

■

Proofgold Proof