proposition: Lemma canonS_iota_i : forall i alpha , nf alpha -> alpha <> zero -> round_n i (iota alpha) (iota (canon alpha (S i))).
proof: Proof. intros i alpha ; transfinite_induction_lt alpha. intros; eapply canonS_iota_final;eauto. intros beta H2 H3 gamma H4; rewrite H4; apply H; eauto with T1. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )