proposition: Lemma path_to_round_plus a s b : path_to b s a -> nf a -> iota a -+-> iota b.
proof: Proof. intros H H0; apply path_to_path_toS in H. now apply path_toS_round_plus with (MoreLists.unshift s). Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )