proposition: Lemma set_ext X Y : sub X Y /\ sub Y X <-> X = Y.
proof: Proof. Proof using ce. destruct (classof_ex X) as [s ->]. destruct (classof_ex Y) as [t ->]. repeat rewrite classof_sub. rewrite classof_eq. split; intros H. - now apply Aeq_ext. - rewrite H. split; firstorder. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)