Let x be given.
Let g and h be given.
Let z be given.
Apply Hgh to the current goal.
An
exact proof term for the current goal is
SNoR_SNoS x Hx z Hz.
Let w be given.
Apply Hgh to the current goal.
An
exact proof term for the current goal is
SNoL_SNoS x Hx w Hw.
rewrite the current goal using L1a (from left to right).
rewrite the current goal using L1b (from left to right).
Use reflexivity.