proposition: Lemma upairAx X Y Z : ele Z (upair X Y) <-> Z = X \/ Z = Y.
proof: Proof. destruct (classof_ex Z) as [u ->]. destruct (classof_ex X) as [s ->]. destruct (classof_ex Y) as [t ->]. repeat rewrite classof_eq. rewrite upair_welldef, classof_ele. apply AupairAx. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)