Let alpha and beta be given.

Assume Ha He.

Let gamma be given.

Assume Hc: gamma ∈ alpha.

We prove the intermediate claim L1: gamma ∈ beta '.

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

We will prove gamma ∈ alpha ∪ {{1}}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hc.

Apply binunionE beta {{1}} gamma L1 to the current goal.

Assume H1: gamma ∈ beta.

An exact proof term for the current goal is H1.

Assume H1: gamma ∈ {{1}}.

We will prove False.

Apply not_ordinal_Sing1 to the current goal.

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

An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hc.

∎