Let n and α be given.
Assume Ha.
Assume H1: α ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.
Apply binunionE {0} {(ordsucc m) '|m ∈ n} α H1 to the current goal.
Assume H2: α ∈ {0}.
An exact proof term for the current goal is SingE 0 α H2.
Assume H2: α ∈ {(ordsucc m) '|m ∈ n}.
We will prove False.
Apply ReplE_impred n (λm ⇒ (ordsucc m) ') α H2 to the current goal.
Let m be given.
Assume Hm: m ∈ n.
Assume H3: α = (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.
∎