Let alpha and beta be given.

Assume Ha Hb.

We prove the intermediate claim L1: ordinal (ordsucc beta).

An exact proof term for the current goal is ordinal_ordsucc beta (ordinal_Hered alpha Ha beta Hb).

Apply ordinal_trichotomy_or alpha (ordsucc beta) Ha L1 to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H2: alpha ∈ ordsucc beta.

We will prove False.

Apply ordsuccE beta alpha H2 to the current goal.

Assume H3: alpha ∈ beta.

An exact proof term for the current goal is In_no2cycle alpha beta H3 Hb.

Assume H3: alpha = beta.

Apply In_irref alpha to the current goal.

rewrite the current goal using H3 (from left to right) at position 1.

An exact proof term for the current goal is Hb.

Assume H2: alpha = ordsucc beta.

Apply orIR to the current goal.

An exact proof term for the current goal is H2.

Assume H2: ordsucc beta ∈ alpha.

Apply orIL to the current goal.

An exact proof term for the current goal is H2.

∎