proposition: Lemma acc_from_to_round_plus alpha beta : nf alpha -> nf beta -> alpha <> 0 -> acc_from alpha beta -> iota alpha -+-> iota beta.
proof: Proof. destruct 4. rewrite path_to_path_toS_iff in H2. eapply path_toS_round_plus; eauto. eapply path_to_not_In_zero; eauto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )