proposition: Lemma DS_iota_3 : forall gamma, nf gamma -> alpha = T1.phi0 (T1.succ gamma) -> round_n i (iota alpha) (iota (canon alpha (S i))).
proof: Proof. intros; subst alpha; rewrite iota_rw3; auto. - simpl iota; rewrite (iota_of_succ gamma); auto. case_eq (iota gamma). right; left; simpl hy_app; left. split; clear H0 ; induction h; auto. + simpl; left. + simpl; right; auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )