Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha.
Assume HaL HaR.
Apply PNo_rel_imv_bdd_ex L R HLR alpha Ha HaL HaR to the current goal.
Let beta be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: beta ∈ ordsucc alpha.
Assume H1.
Apply H1 to the current goal.
Let p be given.
Assume Hp: PNo_rel_strict_split_imv L R beta p.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa beta Hb.
We use beta 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 beta p.
An exact proof term for the current goal is PNo_rel_split_imv_imp_strict_imv L R beta Lb p Hp.
∎