Let α be given.
Assume Ha.
Let x be given.
We prove the intermediate
claim Lx:
SNo x.
An
exact proof term for the current goal is
SNo_SNo α Ha x Hx.
We prove the intermediate
claim Lxa:
SNoLev x = α.
An
exact proof term for the current goal is
SNoLev_uniq2 α Ha x Hx.
We prove the intermediate
claim Lmxa:
SNoLev (- x) = α.
rewrite the current goal using
minus_SNo_Lev x Lx (from left to right).
An exact proof term for the current goal is Lxa.
We will
prove SNo_ α (- x).
rewrite the current goal using Lmxa (from right to left).
∎