Let alpha, beta, p and q be given.
Assume H1.
We will
prove PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta.
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1.
∎