Let alpha and beta be given.

Assume Ha Hb.

Assume H1: beta ' ∈ {gamma '|gamma ∈ alpha}.

Apply ReplE_impred alpha (λgamma ⇒ gamma ') (beta ') H1 to the current goal.

Let gamma be given.

Assume H2: gamma ∈ alpha.

Assume H3: beta ' = gamma '.

We prove the intermediate claim L2: beta = gamma.

An exact proof term for the current goal is tagged_eqE_eq beta gamma Hb (ordinal_Hered alpha Ha gamma H2) H3.

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

An exact proof term for the current goal is H2.

∎