Let α and β be given.

Assume Ha Hb.

Assume H1: β ' ∈ {γ '|γ ∈ α}.

Apply ReplE_impred α (λγ ⇒ γ ') (β ') H1 to the current goal.

Let γ be given.

Assume H2: γ ∈ α.

Assume H3: β ' = γ '.

We prove the intermediate claim L2: β = γ.

An exact proof term for the current goal is tagged_eqE_eq β γ Hb (ordinal_Hered α Ha γ H2) H3.

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

An exact proof term for the current goal is H2.

∎