proposition: Lemma const_pathS_repeat i : forall alpha beta, const_path (S i) alpha beta -> exists n:nat, path_toS beta (repeat i (S n)) alpha.
proof: Proof. induction 1. - exists 0; now left. - destruct IHclos_trans_1n as [n Hn]; exists (S n); now right with y. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)