Let alpha, beta, p and q be given.

Assume H1 H2 H3.

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 or3I3 to the current goal.

Apply and3I to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

An exact proof term for the current goal is H3.

∎