proposition: Lemma const_pathS_repeatR i : forall n alpha beta, path_toS beta (repeat i (S n)) alpha -> const_path (S i) alpha beta.
proof: Proof. induction n. - left; now inversion_clear H. - inversion_clear 1. right with gamma; auto; apply IHn; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)