proposition: Lemma upair_welldef s t : upair (classof s) (classof t) = classof (Aupair s t).
proof: Proof. pose (u := Aupair s t). apply (class_eq (s:=u) (s':=u)); trivial. exists s, t. auto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)