proposition: Lemma DS_iota_2 : forall lambda, nf lambda -> alpha = T1.phi0 lambda -> T1limit lambda -> round_n i (iota alpha) (iota (canon alpha (S i))).
proof: Proof. intros;subst alpha. repeat rewrite iota_phi0; trivial. assert (nz : lambda <> zero). { eapply T1limit_not_zero; eauto. } right; specialize (Hrec lambda nz (head_LT_cons Halpha)). rewrite iota_rw1; trivial. right; left; destruct (Hrec (canon lambda (S i))); auto. assert False by (eapply limit_no_R1; eauto); contradiction. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )