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