Let L and R be given.

Assume HLR.

Let alpha be given.

Assume Ha HaL HaR.

Apply PNo_bd_pred_lem L R HLR alpha Ha HaL HaR to the current goal.

Assume H _.

An exact proof term for the current goal is H.

∎