An exact proof term for the current goal is andI (PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha)) (PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha)) (PNo_lenbdd_strict_imv_extend0 L R alpha Ha HaL HaR p Hp1) (PNo_lenbdd_strict_imv_extend1 L R alpha Ha HaL HaR p Hp1).