Let x, α and β be given.
Assume Ha Hb Hax Hbx.
Let γ be given.
Assume Hc: γ ∈ α.
We will prove γ ∈ β.
Apply Hax to the current goal.
Assume Hax1 Hax2.
Apply Hbx to the current goal.
Assume Hbx1 Hbx2.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered α Ha γ Hc.
Apply exactly1of2_or (γ ' ∈ x) (γ ∈ x) (Hax2 γ Hc) to the current goal.
Assume H1: γ ' ∈ x.
We prove the intermediate claim L1: γ ' ∈ β ∪ {δ '|δ ∈ β}.
An exact proof term for the current goal is Hbx1 (γ ') H1.
We prove the intermediate claim L2: γ ' ∈ β ∨ γ ' ∈ {δ '|δ ∈ β}.
An exact proof term for the current goal is binunionE β {δ '|δ ∈ β} (γ ') L1.
Apply L2 to the current goal.
Assume H2: γ ' ∈ β.
We will prove False.
An exact proof term for the current goal is tagged_notin_ordinal β γ Hb H2.
Assume H2: γ ' ∈ {δ '|δ ∈ β}.
An exact proof term for the current goal is tagged_ReplE β γ Hb Lc H2.
Assume H1: γ ∈ x.
We prove the intermediate claim L1: γ ∈ β ∪ {δ '|δ ∈ β}.
An exact proof term for the current goal is Hbx1 γ H1.
We prove the intermediate claim L2: γ ∈ β ∨ γ ∈ {δ '|δ ∈ β}.
An exact proof term for the current goal is binunionE β {δ '|δ ∈ β} γ L1.
Apply L2 to the current goal.
Assume H2: γ ∈ β.
An exact proof term for the current goal is H2.
Assume H2: γ ∈ {δ '|δ ∈ β}.
We will prove False.
An exact proof term for the current goal is ordinal_notin_tagged_Repl γ β Lc H2.
∎