proposition: Lemma AP_omega : In AP omega.
proof: Proof. repeat split. - apply lt_trans with (F 1). + simpl (F 1) ; auto with schutte. + apply finite_lt_omega. - intros beta H; case (@lt_omega_finite _ H). intros;subst beta;apply finite_plus_infinite; auto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)