Let alpha and p be given.

Set p1 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 ↔ p1 beta.

Apply iffI to the current goal.

Assume H1: p beta.

We will prove p beta ∨ beta = alpha.

Apply orIL to the current goal.

An exact proof term for the current goal is H1.

Assume H1: p1 beta.

Apply H1 to the current goal.

Assume H2: p beta.

An exact proof term for the current goal is H2.

Assume H2: beta = alpha.

We will prove False.

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.

∎