Let L and R be given.
Assume HLR.
Let p be given.
Assume Hp.
Apply SNoCutP_SNoCut L R HLR to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
An exact proof term for the current goal is Hp.