Let x0 of type ι be given.

Assume H0: nat_p x0.

Let x1 of type ι → ο be given.

Assume H1: x1 0.

Assume H2: x1 1.

Assume H3: ∀ x2 . x2 ∈ setminus omega 2 ⟶ x1 x2.

Apply nat_inv with x0, x1 x0 leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H4: x0 = 0.

Apply H4 with λ x2 x3 . x1 x3.

The subproof is completed by applying H1.

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

Apply H4 with x1 x0.

Let x2 of type ι be given.

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

Apply H5 with x1 x0.

Assume H6: nat_p x2.

Assume H7: x0 = ordsucc x2.

Apply H7 with λ x3 x4 . x1 x4.

Apply nat_inv with x2, x1 (ordsucc x2) leaving 3 subgoals.

The subproof is completed by applying H6.

Assume H8: x2 = 0.

Apply H8 with λ x3 x4 . x1 (ordsucc x4).

The subproof is completed by applying H2.

Assume H8: ∃ x3 . and (nat_p x3) (x2 = ordsucc x3).

Apply H8 with x1 (ordsucc x2).

Let x3 of type ι be given.

Assume H9: (λ x4 . and (nat_p x4) (x2 = ordsucc x4)) x3.

Apply H9 with x1 (ordsucc x2).

Assume H10: nat_p x3.

Assume H11: x2 = ordsucc x3.

Apply H11 with λ x4 x5 . x1 (ordsucc x5).

Apply H3 with ordsucc (ordsucc x3).

Apply setminusI with omega, 2, ordsucc (ordsucc x3) leaving 2 subgoals.

Apply nat_p_omega with ordsucc (ordsucc x3).

Apply nat_ordsucc with ordsucc x3.

Apply nat_ordsucc with x3.

The subproof is completed by applying H10.

Assume H12: ordsucc (ordsucc x3) ∈ 2.

Claim L13: not (or (ordsucc (ordsucc x3) = 0) (ordsucc (ordsucc x3) = 1))

Assume H13: or (ordsucc (ordsucc x3) = 0) (ordsucc (ordsucc x3) = 1).

Apply H13 with False leaving 2 subgoals.

The subproof is completed by applying neq_ordsucc_0 with ordsucc x3.

Apply ordsucc_inj_contra with ordsucc x3, 0.

The subproof is completed by applying neq_ordsucc_0 with x3.

Apply L13.

Apply cases_2 with ordsucc (ordsucc x3), λ x4 . or (x4 = 0) (x4 = 1) leaving 3 subgoals.

The subproof is completed by applying H12.

Apply orIL with 0 = 0, 0 = 1.

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

Assume H14: x4 0 0.

The subproof is completed by applying H14.

Apply orIR with 1 = 0, 1 = 1.

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

Assume H14: x4 1 1.

The subproof is completed by applying H14.

■

Proofgold Proof