Let γ be given.
We prove the intermediate
claim Lgamma:
ordinal γ.
An
exact proof term for the current goal is
ordinal_Hered α Ha γ H5.
We prove the intermediate
claim L1:
β = γ.
An
exact proof term for the current goal is
tagged_eqE_eq β γ Lbeta Lgamma H7.
Apply H6 to the current goal.
We will prove p γ.
rewrite the current goal using L1 (from right to left).
We will prove p β.
An exact proof term for the current goal is H2.