proposition: Lemma iota_rw1 : forall i alpha, nf alpha -> T1limit alpha = true -> iota (canon (cons alpha 0 zero) (S i)) = hyd1 (iota (canon alpha (S i))).
proof: Proof. intros i alpha H H0; rewrite canonS_lim1; auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )