Let n and alpha be given.
Assume Ha.
Assume H1: alpha ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.
Apply binunionE {0} {(ordsucc m) '|m ∈ n} alpha H1 to the current goal.
Assume H2: alpha ∈ {0}.
An exact proof term for the current goal is SingE 0 alpha H2.
Assume H2: alpha ∈ {(ordsucc m) '|m ∈ n}.
We will prove False.
Apply ReplE_impred n (λm ⇒ (ordsucc m) ') alpha H2 to the current goal.
Let m be given.
Assume Hm: m ∈ n.
Assume H3: alpha = (ordsucc m) '.
Apply tagged_not_ordinal (ordsucc m) to the current goal.
We will prove ordinal ((ordsucc m) ').
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is Ha.
∎