proposition: Lemma om_Ax2 : forall X, inductive X -> sub om X.
proof: Proof. intros X H. destruct (classof_ex X) as [s ->]. apply classof_sub. now apply AomAx2, Ainductive_inductive. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)