Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: nat_p x0.

Assume H1: nat_p x1.

Apply nat_inv with x1, add_nat x0 x1 ⊆ x0 ⟶ x1 = 0 leaving 3 subgoals.

The subproof is completed by applying H1.

Assume H2: x1 = 0.

Assume H3: add_nat x0 x1 ⊆ x0.

The subproof is completed by applying H2.

Assume H2: ∃ x2 . and (nat_p x2) (x1 = ordsucc x2).

Apply H2 with add_nat x0 x1 ⊆ x0 ⟶ x1 = 0.

Let x2 of type ι be given.

Assume H3: (λ x3 . and (nat_p x3) (x1 = ordsucc x3)) x2.

Apply H3 with add_nat x0 x1 ⊆ x0 ⟶ x1 = 0.

Assume H4: nat_p x2.

Assume H5: x1 = ordsucc x2.

Apply H5 with λ x3 x4 . add_nat x0 x4 ⊆ x0 ⟶ x4 = 0.

Apply add_nat_SR with x0, x2, λ x3 x4 . x4 ⊆ x0 ⟶ ordsucc x2 = 0 leaving 2 subgoals.

The subproof is completed by applying H4.

Assume H6: ordsucc (add_nat x0 x2) ⊆ x0.

Apply FalseE with ordsucc x2 = 0.

Apply In_irref with x0.

Apply H6 with x0.

Apply unknownprop_65854e80dcdfdaad216d9278c1826bfa6e412eacf7818f3d49e43d93a23f7bcf with x0, x2.

The subproof is completed by applying H4.

■

Proofgold Proof