proposition: Lemma Ainductive_inductive s : Ainductive s <-> inductive (classof s).
proof: Proof. split; intros H. - split. + apply classof_ele. apply H. + intros X H'. destruct (classof_ex X) as [t ->]. rewrite succ_eq. apply classof_ele, H. now apply classof_ele. - split. + apply classof_ele. apply H. + intros t Ht. apply classof_ele. rewrite <- succ_eq. apply H. now apply classof_ele. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)