Apply nat_ind with λ x0 . ∀ x1 . nat_p x1 ⟶ x0 ⊆ x1 ⟶ ∃ x2 . and (nat_p x2) (x1 = add_nat x2 x0) leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: 0 ⊆ x0.

Let x1 of type ο be given.

Assume H2: ∀ x2 . and (nat_p x2) (x0 = add_nat x2 0) ⟶ x1.

Apply H2 with x0.

Apply andI with nat_p x0, x0 = add_nat x0 0 leaving 2 subgoals.

The subproof is completed by applying H0.

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

The subproof is completed by applying add_nat_0R with x0, λ x3 x4 . x2 x4 x3.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . nat_p x1 ⟶ x0 ⊆ x1 ⟶ ∃ x2 . and (nat_p x2) (x1 = add_nat x2 x0).

Apply nat_inv_impred with λ x1 . ordsucc x0 ⊆ x1 ⟶ ∃ x2 . and (nat_p x2) (x1 = add_nat x2 (ordsucc x0)) leaving 2 subgoals.

Assume H2: ordsucc x0 ⊆ 0.

Apply FalseE with ∃ x1 . and (nat_p x1) (0 = add_nat x1 (ordsucc x0)).

Apply EmptyE with x0.

Apply H2 with x0.

The subproof is completed by applying ordsuccI2 with x0.

Let x1 of type ι be given.

Assume H2: nat_p x1.

Assume H3: ordsucc x0 ⊆ ordsucc x1.

Apply H1 with x1, ∃ x2 . and (nat_p x2) (ordsucc x1 = add_nat x2 (ordsucc x0)) leaving 3 subgoals.

The subproof is completed by applying H2.

Apply ordinal_In_Or_Subq with x1, x0, x0 ⊆ x1 leaving 4 subgoals.

Apply nat_p_ordinal with x1.

The subproof is completed by applying H2.

Apply nat_p_ordinal with x0.

The subproof is completed by applying H0.

Assume H4: x1 ∈ x0.

Apply FalseE with x0 ⊆ x1.

Apply In_irref with ordsucc x1.

Apply H3 with ordsucc x1.

Apply nat_ordsucc_in_ordsucc with x0, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H4.

Assume H4: x0 ⊆ x1.

The subproof is completed by applying H4.

Let x2 of type ι be given.

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

Apply H4 with ∃ x3 . and (nat_p x3) (ordsucc x1 = add_nat x3 (ordsucc x0)).

Assume H5: nat_p x2.

Assume H6: x1 = add_nat x2 x0.

Let x3 of type ο be given.

Assume H7: ∀ x4 . and (nat_p x4) (ordsucc x1 = add_nat x4 (ordsucc x0)) ⟶ x3.

Apply H7 with x2.

Apply andI with nat_p x2, ordsucc x1 = add_nat x2 (ordsucc x0) leaving 2 subgoals.

The subproof is completed by applying H5.

Apply add_nat_SR with x2, x0, λ x4 x5 . ordsucc x1 = x5 leaving 2 subgoals.

The subproof is completed by applying H0.

set y4 to be ordsucc (add_nat x2 x0)

Claim L8: ∀ x5 : ι → ο . x5 y4 ⟶ x5 (ordsucc x1)

Let x5 of type ι → ο be given.

The subproof is completed by applying H6 with λ x6 x7 . (λ x8 . x5) (ordsucc x6) (ordsucc x7).

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

Apply L8 with λ x6 . x5 x6 y4 ⟶ x5 y4 x6.

Assume H9: x5 y4 y4.

The subproof is completed by applying H9.

■

Proofgold Proof