proposition: Lemma iota_rw4 : forall i n alpha , nf alpha -> iota (canon (cons (T1.succ alpha) (S n) zero) (S i)) = node (hcons_mult (iota (T1.succ alpha)) (S n) (hcons_mult (iota alpha) (S i) hnil)).
proof: Proof. intros i n alpha H; rewrite canonS_cons_succ_eqn2; auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )