proposition: Lemma classof_eq s t : classof s = classof t <-> Aeq s t.
proof: Proof. Proof using ce. split; intros H. - specialize (classof_class s). intros XX. rewrite H in XX. symmetry. exact XX. - apply (class_eq H); simpl; trivial. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)