Assume H1: ¬ PNoEq_ α p q.

We prove the intermediate claim L1: ∃β, ¬ (β ∈ α → (p β ↔ q β)).

An exact proof term for the current goal is not_all_ex_demorgan_i (λβ ⇒ β ∈ α → (p β ↔ q β)) H1.

Apply L1 to the current goal.

Let β be given.

Assume H2: ¬ (β ∈ α → (p β ↔ q β)).

We prove the intermediate claim L2: β ∈ α ∧ ¬ (p β ↔ q β).

Apply xm (β ∈ α) to the current goal.

Assume H3: β ∈ α.

Apply xm (p β ↔ q β) to the current goal.

Assume H4: p β ↔ q β.

We will prove False.

Apply H2 to the current goal.

Assume _.

An exact proof term for the current goal is H4.

Assume H4: ¬ (p β ↔ q β).

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H4.

Assume H3: β ∉ α.

We will prove False.

Apply H2 to the current goal.

Assume H4.

We will prove False.

An exact proof term for the current goal is H3 H4.

Apply L2 to the current goal.

Assume H3: β ∈ α.

Assume H4: ¬ (p β ↔ q β).

Apply IH β H3 to the current goal.

Assume H5.

Apply H5 to the current goal.

Assume H5: PNoLt_ β p q.

Apply orIL to the current goal.

An exact proof term for the current goal is PNoLt_mon_ p q α Ha β H3 H5.

Assume H5: PNoEq_ β p q.

Apply xm (p β) to the current goal.

Assume H6: p β.

Apply xm (q β) to the current goal.

Assume H7: q β.

We will prove False.

Apply H4 to the current goal.

Apply iffI to the current goal.

Assume _.

An exact proof term for the current goal is H7.

Assume _.

An exact proof term for the current goal is H6.

Assume H7: ¬ q β.

Apply orIR to the current goal.

We will prove ∃β ∈ α, PNoEq_ β q p ∧ ¬ q β ∧ p β.

We use β to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

Apply and3I to the current goal.

Apply PNoEq_sym_ to the current goal.

An exact proof term for the current goal is H5.

An exact proof term for the current goal is H7.

An exact proof term for the current goal is H6.

Assume H6: ¬ p β.

Apply xm (q β) to the current goal.

Assume H7: q β.

Apply orIL to the current goal.

We will prove ∃β ∈ α, PNoEq_ β p q ∧ ¬ p β ∧ q β.

We use β to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

Apply and3I to the current goal.

An exact proof term for the current goal is H5.

An exact proof term for the current goal is H6.

An exact proof term for the current goal is H7.

Assume H7: ¬ q β.

We will prove False.

Apply H4 to the current goal.

Apply iffI to the current goal.

Assume H8.

We will prove False.

An exact proof term for the current goal is H6 H8.

Assume H8.

We will prove False.

An exact proof term for the current goal is H7 H8.

Assume H5: PNoLt_ β q p.

Apply orIR to the current goal.

An exact proof term for the current goal is PNoLt_mon_ q p α Ha β H3 H5.