Let L and R be given.
Assume HLR.
Let α be given.
Assume Ha.
Assume HaL HaR.
Apply PNo_rel_imv_bdd_ex L R HLR α Ha HaL HaR to the current goal.
Let β be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: β ∈ ordsucc α.
Assume H1.
Apply H1 to the current goal.
Let p be given.
Assume Hp: PNo_rel_strict_split_imv L R β p.
We prove the intermediate claim Lsa: ordinal (ordsucc α).
An exact proof term for the current goal is ordinal_ordsucc α Ha.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered (ordsucc α) Lsa β Hb.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
We use p to witness the existential quantifier.
We will prove PNo_strict_imv L R β p.
An exact proof term for the current goal is PNo_rel_split_imv_imp_strict_imv L R β Lb p Hp.
∎