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