proposition: Theorem AP_unbounded : Unbounded AP.
proof: Proof. intro x. exists (omega_limit (fix seq (n : nat) : Ord := match n with | O => succ x | S p => seq p + seq p end)). destruct (AP_unbounded_0 x); now split. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)