Let α and p be given.

Set p1 to be the term λδ ⇒ p δ ∨ δ = α of type set → prop.

Let β be given.

Assume Hb: β ∈ α.

We will prove p β ↔ p1 β.

Apply iffI to the current goal.

Assume H1: p β.

We will prove p β ∨ β = α.

Apply orIL to the current goal.

An exact proof term for the current goal is H1.

Assume H1: p1 β.

Apply H1 to the current goal.

Assume H2: p β.

An exact proof term for the current goal is H2.

Assume H2: β = α.

We will prove False.

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.

∎