Let L and R be given.

Assume HLR.

Let alpha be given.

Assume Ha HaL HaR.

An exact proof term for the current goal is DescrR_i_io_12 (PNo_least_rep2 L R) (PNo_lenbdd_least_rep2_exuniq2 L R HLR alpha Ha HaL HaR).

∎