proposition: Lemma iota_rw2 : forall i n alpha, nf alpha -> T1limit alpha = true -> iota (canon (cons alpha (S n) zero) (S i)) = node (hcons_mult (iota alpha) (S n) (hcons (iota (canon alpha (S i))) hnil)).
proof: Proof. intros i n alpha H H0; rewrite canonS_lim2; auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )