Let p, q and alpha be given.

Assume Ha.

Let beta be given.

Assume Hb H1.

Apply H1 to the current goal.

Let gamma be given.

Assume H2.

Apply H2 to the current goal.

Assume H2: gamma ∈ beta.

Assume H3.

We will prove ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta.

We use gamma to witness the existential quantifier.

Apply andI to the current goal.

We will prove gamma ∈ alpha.

Apply Ha to the current goal.

Assume Ha1 _.

An exact proof term for the current goal is Ha1 beta Hb gamma H2.

An exact proof term for the current goal is H3.

∎