proposition: Lemma path_toS_round_plus alpha s beta : path_toS beta s alpha -> nf alpha -> iota alpha -+-> iota beta.
proof: Proof. intros; apply trace_to_round_plus with s. now apply path_toS_trace. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )