Apply nat_inv_impred to the current goal.

Assume _.

Apply orIL to the current goal.

Use reflexivity.

Apply nat_inv_impred to the current goal.

Assume _.

Apply orIR to the current goal.

Use reflexivity.

Let m be given.

Assume Hm.

Assume H1: ordsucc (ordsucc m) ⊆ 1.

We will prove False.

Apply In_irref 1 to the current goal.

We will prove 1 ∈ 1.

Apply H1 to the current goal.

We will prove 1 ∈ ordsucc (ordsucc m).

Apply nat_ordsucc_in_ordsucc (ordsucc m) (nat_ordsucc m Hm) to the current goal.

We will prove 0 ∈ ordsucc m.

An exact proof term for the current goal is nat_0_in_ordsucc m Hm.

∎