Let x, alpha and beta be given.
Assume Ha Hb Hax Hbx.
Let gamma be given.
Assume Hc: gamma ∈ alpha.
We will prove gamma ∈ beta.
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 gamma.
An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hc.
Apply exactly1of2_or (gamma ' ∈ x) (gamma ∈ x) (Hax2 gamma Hc) to the current goal.
Assume H1: gamma ' ∈ x.
We prove the intermediate claim L1: gamma ' ∈ beta ∪ {delta '|delta ∈ beta}.
An exact proof term for the current goal is Hbx1 (gamma ') H1.
We prove the intermediate claim L2: gamma ' ∈ beta ∨ gamma ' ∈ {delta '|delta ∈ beta}.
An exact proof term for the current goal is binunionE beta {delta '|delta ∈ beta} (gamma ') L1.
Apply L2 to the current goal.
Assume H2: gamma ' ∈ beta.
We will prove False.
An exact proof term for the current goal is tagged_notin_ordinal beta gamma Hb H2.
Assume H2: gamma ' ∈ {delta '|delta ∈ beta}.
An exact proof term for the current goal is tagged_ReplE beta gamma Hb Lc H2.
Assume H1: gamma ∈ x.
We prove the intermediate claim L1: gamma ∈ beta ∪ {delta '|delta ∈ beta}.
An exact proof term for the current goal is Hbx1 gamma H1.
We prove the intermediate claim L2: gamma ∈ beta ∨ gamma ∈ {delta '|delta ∈ beta}.
An exact proof term for the current goal is binunionE beta {delta '|delta ∈ beta} gamma L1.
Apply L2 to the current goal.
Assume H2: gamma ∈ beta.
An exact proof term for the current goal is H2.
Assume H2: gamma ∈ {delta '|delta ∈ beta}.
We will prove False.
An exact proof term for the current goal is ordinal_notin_tagged_Repl gamma beta Lc H2.
∎