proposition: Lemma canonS_rel_rounds : forall n alpha beta, nf alpha -> nf beta -> alpha <> zero -> beta = canon alpha (S n) -> iota alpha -+-> iota beta.
proof: Proof. inversion 4; subst; left; apply canonS_iota; auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )