proposition: Lemma path_to_path_toS_iff : forall alpha s beta, ~ In 0 s -> path_to beta s alpha <-> path_toS beta (unshift s) alpha.
proof: Proof. split. - apply path_to_path_toS. - rewrite <- (unshift_shift s); auto. repeat rewrite shift_unshift. apply path_toS_path_to. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)