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