An exact proof term for the current goal is PNoEq_sym_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y).