Let z be given.
Let w be given.
rewrite the current goal using Hzw (from left to right).
Apply SNoR_E x Hx w Hw to the current goal.
rewrite the current goal using
minus_SNo_Lev w Hw1 (from left to right).
rewrite the current goal using
minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is Hw2.
An exact proof term for the current goal is Hw3.
∎