Let α and y be given.

Assume H1 H2.

Apply tagged_not_ordinal y to the current goal.

An exact proof term for the current goal is ordinal_Hered α H1 (y ') H2.

∎