proposition: Lemma DS_iota_1 : forall gamma, nf gamma -> alpha = T1.succ gamma -> round_n i (iota alpha) (iota (canon alpha (S i))).
proof: Proof. intros; subst alpha; rewrite canonS_succ; auto. now apply iota_succ_round_n. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )