proposition: Lemma om_Ax1 : inductive om.
proof: Proof. split. - apply classof_ele. apply AomAx1. - intros X H. destruct (classof_ex X) as [s ->]. rewrite succ_eq. apply classof_ele, AomAx1. now apply classof_ele. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)