Apply nat_inv_impred to the current goal.

Assume _.

Apply orIL to the current goal.

Apply orIL to the current goal.

Use reflexivity.

Apply nat_inv_impred to the current goal.

Assume _.

Apply orIL to the current goal.

Apply orIR 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 (ordsucc m)) ⊆ 2.

We will prove False.

Apply In_irref 2 to the current goal.

We will prove 2 ∈ 2.

Apply H1 to the current goal.

We will prove 2 ∈ ordsucc (ordsucc (ordsucc m)).

Apply nat_ordsucc_in_ordsucc (ordsucc (ordsucc m)) (nat_ordsucc (ordsucc m) (nat_ordsucc m Hm)) 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.

∎