Let L and R be given.

Assume H1: SNoCutP L R.

Apply SNoCutP_SNoCut L R H1 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume H2 _.

An exact proof term for the current goal is H2.

∎