Let α, β, p and q be given.

Assume H1 H2 H3.

We will prove PNoLt_ (α ∩ β) p q ∨ α ∈ β ∧ PNoEq_ α p q ∧ q α ∨ β ∈ α ∧ PNoEq_ β p q ∧ ¬ p β.

Apply or3I2 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.

∎