proposition: Lemma gnaw_path_to : forall s alpha , s <> nil -> ~ In 0 s -> gnaw alpha s <> zero -> path_to (gnaw alpha s) s alpha.
proof: Proof. intros s alpha H H0. replace s with (shift (unshift s)). 2: apply unshift_shift; assumption. rewrite <- gnawS_gnaw. intros; apply path_toS_path_to. apply gnawS_path_toS; auto. clear alpha H1. revert H H0. induction s; simpl; auto. destruct a. tauto. discriminate. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)