Let α and β be given.
Assume Ha Hb Hab.
We prove the intermediate
claim L1:
α ∈ ordsucc β.
An exact proof term for the current goal is H1.
We prove the intermediate
claim L1a:
α = β.
An exact proof term for the current goal is Hab.
An exact proof term for the current goal is H1.
rewrite the current goal using L1a (from left to right).
We prove the intermediate
claim La1:
SNo α.
An
exact proof term for the current goal is
ordinal_SNo α Ha.
We prove the intermediate
claim La2:
SNoLev α = α.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is L1.
∎