Let L, R and α be given.
Assume Ha.
Let p and β be given.
Assume Hb H1.
Apply H1 to the current goal.
Assume H2 H3.
We will prove PNo_rel_strict_upperbd L β p ∧ PNo_rel_strict_lowerbd R β p.
Apply andI to the current goal.
An exact proof term for the current goal is PNo_rel_strict_upperbd_antimon L α Ha p β Hb H2.
An exact proof term for the current goal is PNo_rel_strict_lowerbd_antimon R α Ha p β Hb H3.
∎