Let L and R be given.

Assume HLR.

Let α be given.

Assume Ha HaL HaR.

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

Assume H _.

An exact proof term for the current goal is H.

∎