proposition: Lemma upair_eqclass X Y : eqclass (upair' X Y).
proof: Proof. Proof using ce. destruct (classof_ex X) as [s ->]. destruct (classof_ex Y) as [t ->]. exists (Aupair s t). apply ce. intros z. split; intros H. - destruct H as [s'[t'[H1[H2 H3]]]]; simpl in H1, H2. now rewrite H1, H2, H3. - exists s, t. simpl. repeat split; auto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)