proposition: Lemma succ_is_plus_1 alpha : succ alpha = alpha + 1.
proof: Proof. rewrite <- alpha_plus_zero at 1; change (F 1) with (succ zero). rewrite plus_of_succ; now repeat rewrite alpha_plus_zero. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)