proposition: Lemma plus_FF : forall i j, F (i + j) = F i + F j.
proof: Proof. induction i. - simpl. intros;rewrite zero_plus_alpha;auto with schutte. - simpl; induction j. + simpl. rewrite alpha_plus_zero;auto with schutte. now rewrite <- (plus_n_O i). + rewrite IHi. replace (F (S j)) with (succ (F j)). * rewrite plus_of_succ, plus_of_succ, <- IHi, IHj; auto with schutte. * now simpl. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)