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