Let n be given.
Assume H1.
Apply (H1 (λn ⇒ ∀m ∈ n, ordsucc m ∈ ordsucc n)) to the current goal.
We will prove ∀m ∈ 0, ordsucc m ∈ ordsucc 0.
Let m be given.
Assume Hm: m ∈ 0.
We will prove False.
An exact proof term for the current goal is (EmptyE m Hm).
Let n be given.
Assume IH: ∀m ∈ n, ordsucc m ∈ ordsucc n.
We will prove ∀m ∈ ordsucc n, ordsucc m ∈ ordsucc (ordsucc n).
Let m be given.
Assume H2: m ∈ ordsucc n.
We will prove ordsucc m ∈ ordsucc (ordsucc n).
Apply (ordsuccE n m H2) to the current goal.
Assume H3: m ∈ n.
We prove the intermediate claim L1: ordsucc m ∈ ordsucc n.
An exact proof term for the current goal is (IH m H3).
An exact proof term for the current goal is (ordsuccI1 (ordsucc n) (ordsucc m) L1).
Assume H3: m = n.
rewrite the current goal using H3 (from left to right).
We will prove ordsucc n ∈ ordsucc (ordsucc n).
An exact proof term for the current goal is (ordsuccI2 (ordsucc n)).
∎