Apply In_ind to the current goal.

We will prove (∀X : set, (∀x : set, x ∈ X → x ∉ x) → X ∉ X).

Let X be given.

Assume IH: ∀x : set, x ∈ X → x ∉ x.

Assume H: X ∈ X.

An exact proof term for the current goal is IH X H H.

∎