proposition: Lemma classof_sub s t : sub (classof s) (classof t) <-> ASubq s t.
proof: Proof. Proof using ce. split; intros H1. - intros u H2. now apply classof_ele, H1, classof_ele. - intros Z H2. destruct (classof_ex Z) as [u ->]. now apply classof_ele, H1, classof_ele. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)