Apply In_ind to the current goal.

Let x be given.

Assume IH: ∀z, z ∈ x → ∀y, z ∈ y → y ∈ z → False.

Let y be given.

Assume H1: x ∈ y.

Assume H2: y ∈ x.

An exact proof term for the current goal is IH y H2 x H2 H1.

∎