proposition: Lemma classof_ele s t : ele (classof s) (classof t) <-> Ain s t.
proof: Proof. split; intros H. - apply H; simpl; auto. - intros s' t' H1 H2. now rewrite <- H1, <- H2. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)