proposition: Lemma iota_of_succ : forall beta, nf beta -> iota (T1.succ beta) = match (iota beta) with node s => node (hy_app s (hcons head hnil)) end.
proof: Proof. intros; rewrite <- iota_iotas; auto. rewrite (iotas_succ); auto. rewrite <- iota_iotas; auto. apply succ_nf;auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )