Let L, R and α be given.
Assume Ha: ordinal α.
Let β be given.
Assume Hb: β ∈ ordsucc α.
Let p be given.
Assume H1: PNo_strict_imv L R α p.
Apply H1 to the current goal.
Assume H2: PNo_strict_upperbd L α p.
Assume H3: PNo_strict_lowerbd R α p.
We will prove PNo_rel_strict_imv L R β p.
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_strict_upperbd_imp_rel_strict_upperbd L α Ha β Hb p H2.
An exact proof term for the current goal is PNo_strict_lowerbd_imp_rel_strict_lowerbd R α Ha β Hb p H3.
∎