Let alpha and p be given.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop.
Let beta be given.
Assume Hb: beta ∈ alpha.
We will prove p beta ↔ p0 beta.
Apply iffI to the current goal.
Assume H1: p beta.
We will prove p beta ∧ beta ≠ alpha.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
We will prove beta ≠ alpha.
Assume H2: beta = alpha.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is Hb.
Assume H1: p0 beta.
Apply H1 to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2.
∎