Let w be given.
Assume Hw.
Let z be given.
Assume Hz.
Let m be given.
rewrite the current goal using
SingE 0 w Hw (from left to right).
rewrite the current goal using Hm2 (from left to right).
An
exact proof term for the current goal is
nat_p_trans n Ln m Hm1.
∎