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