proposition: Lemma o2iota : forall alpha , nf alpha -> forall i, (0 < i)%nat -> alpha = T1.zero \/ exists k : nat, rounds standard (Nat.pred i) (iota alpha) k head .
proof: Proof. intros alpha; transfinite_induction_lt alpha. intros x H H0 i H1; destruct (T1_eq_dec x T1.zero). - now left. - right; destruct i. + inversion H1. + specialize (H (canon x (S i)) H0); assert (nf (canon x (S i))) by (eapply nf_canon; eauto). assert (T1.lt (canon x (S i)) x). { eapply canon_lt; eauto. } specialize (H H2 H3 H2 (S (S i)) ). destruct H. * auto with arith. * destruct (canonS_zero_inv _ _ H). subst; now destruct n. subst; exists (S i); simpl; left. { left; split; now left. } * simpl; destruct H; exists x0. eapply rounds_trans with (S i) (iota (canon x (S i))). { simpl; simpl in H; trivial. } { left. eapply canonS_iota_i; auto. } Qed.
imports: hydras(Epsilon0_Needed_Generic)