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