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