proposition: Lemma classof_ex X : exists s, X = classof s.
proof: Proof. Proof using ce. destruct X as [P[s ->]]; simpl. exists s. apply (@class_eq _ _ s s); simpl; auto; reflexivity. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)