Apply nat_ind with λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0 leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: x0 ∈ 0.

Apply FalseE with x0 ⊆ 0.

Apply EmptyE with x0.

The subproof is completed by applying H0.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0.

Let x1 of type ι be given.

Assume H2: x1 ∈ ordsucc x0.

Apply ordsuccE with x0, x1, x1 ⊆ ordsucc x0 leaving 3 subgoals.

The subproof is completed by applying H2.

Assume H3: x1 ∈ x0.

Apply Subq_tra with x1, x0, ordsucc x0 leaving 2 subgoals.

Apply H1 with x1.

The subproof is completed by applying H3.

The subproof is completed by applying ordsuccI1 with x0.

Assume H3: x1 = x0.

Apply H3 with λ x2 x3 . x3 ⊆ ordsucc x0.

The subproof is completed by applying ordsuccI1 with x0.

■

Proofgold Proof