proposition: Lemma inject_of_finite_pos : forall n, inject (\F (S n)) = F (S n).
proof: Proof. induction n;simpl. - rewrite phi0_zero. rewrite alpha_plus_zero; auto with schutte. - clear IHn. induction n; simpl ; auto. + repeat rewrite phi0_zero. rewrite alpha_plus_zero; auto with schutte. * rewrite <- succ_is_plus_1. f_equal. + rewrite alpha_plus_zero. * rewrite alpha_plus_zero in IHn. rewrite IHn. replace (AP._phi0 zero) with (F 1). rewrite <- succ_is_plus_1; auto with schutte. symmetry; auto with schutte. apply phi0_zero. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)