proposition: Lemma iota_tail : forall i alpha n beta, nf (cons alpha n beta) -> beta <> zero -> iota (canon (cons alpha n beta) (S i)) = node (hcons_mult (iota alpha) (S n) (iotas (canon beta (S i)))).
proof: Proof. intros i alpha n beta H H0; rewrite canon_tail; auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )