Let a be given.

We will prove ¬ (0 = ordsucc a).

Assume H1: 0 = ordsucc a.

We prove the intermediate claim L1: a ∈ ordsucc a → False.

rewrite the current goal using H1 (from right to left).

An exact proof term for the current goal is (EmptyE a).

An exact proof term for the current goal is (L1 (ordsuccI2 a)).

∎