Let L and R be given.
Let α be given.
Assume Ha.
Assume HaL HaR.
Let p be given.
Assume Hp1.
We will prove PNo_rel_strict_split_imv L R α p.
An exact proof term for the current goal is andI (PNo_rel_strict_imv L R (ordsucc α) (λδ ⇒ p δ ∧ δ ≠ α)) (PNo_rel_strict_imv L R (ordsucc α) (λδ ⇒ p δ ∨ δ = α)) (PNo_lenbdd_strict_imv_extend0 L R α Ha HaL HaR p Hp1) (PNo_lenbdd_strict_imv_extend1 L R α Ha HaL HaR p Hp1).
∎