Let α and β be given.

Assume Ha He.

Let γ be given.

Assume Hc: γ ∈ α.

We prove the intermediate claim L1: γ ∈ β '.

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

We will prove γ ∈ α ∪ {{1}}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hc.

Apply binunionE β {{1}} γ L1 to the current goal.

Assume H1: γ ∈ β.

An exact proof term for the current goal is H1.

Assume H1: γ ∈ {{1}}.

We will prove False.

Apply not_ordinal_Sing1 to the current goal.

rewrite the current goal using SingE {1} γ H1 (from right to left).

An exact proof term for the current goal is ordinal_Hered α Ha γ Hc.

∎