Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume HaL HaR.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
Apply PNo_rel_imv_ex L R HLR alpha Ha to the current goal.
Assume H2.
Apply H2 to the current goal.
Let p be given.
Assume Hp: PNo_rel_strict_uniq_imv L R alpha p.
Apply Hp to the current goal.
Assume Hp1: PNo_rel_strict_imv L R alpha p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Assume Hp2: ∀q : set → prop, PNo_rel_strict_imv L R alpha q → PNoEq_ alpha p q.
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
We will prove alpha ∈ ordsucc alpha.
Apply ordsuccI2 to the current goal.
We use p to witness the existential quantifier.
We will prove PNo_rel_strict_split_imv L R alpha p.
An exact proof term for the current goal is PNo_lenbdd_strict_imv_split L R alpha Ha HaL HaR p Hp1.
Assume H1.
Apply H1 to the current goal.
Let beta be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: beta ∈ alpha.
Assume H1.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
We will prove beta ∈ ordsucc alpha.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is H1.
∎