proposition: Lemma path_to_gnaw : forall s alpha beta, path_to beta s alpha -> beta = gnaw alpha s.
proof: Proof. intros. assert (H0: ~ In 0 s). { now apply path_to_not_In_zero in H. } generalize (unshift_shift s H0); intro e. rewrite gnaw_gnawS; apply path_toS_gnawS. now apply path_to_path_toS in H. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)