Let α and Y be given.

Assume H1: ordinal α.

Assume H2: α ∈ {y '|y ∈ Y}.

Apply ReplE_impred Y (λy ⇒ y ') α H2 to the current goal.

Let y be given.

Assume H3: y ∈ Y.

Assume H4: α = y '.

Apply tagged_not_ordinal y to the current goal.

We will prove ordinal (y ').

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

An exact proof term for the current goal is H1.

∎