Let n be given.

Assume H1.

Apply H1 (λn ⇒ 0 ∈ ordsucc n) to the current goal.

We will prove 0 ∈ ordsucc 0.

An exact proof term for the current goal is In_0_1.

Let n be given.

Assume IH: 0 ∈ ordsucc n.

We will prove 0 ∈ ordsucc (ordsucc n).

An exact proof term for the current goal is (ordsuccI1 (ordsucc n) 0 IH).

∎