Let α and p be given.
Set p0 to be the term λδ ⇒ p δ ∧ δ ≠ α of type set → prop.
Let β be given.
Assume Hb: β ∈ α.
We will prove p β ↔ p0 β.
Apply iffI to the current goal.
Assume H1: p β.
We will prove p β ∧ β ≠ α.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
We will prove β ≠ α.
Assume H2: β = α.
Apply In_irref α 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 β.
Apply H1 to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2.
∎