proposition: Lemma gnawS_path_toS : forall s alpha , s <> nil -> gnawS alpha s <> zero -> path_toS (gnawS alpha s) s alpha.
proof: Proof. induction s. - now destruct 1. - destruct s. + left. split. intro; subst. simpl in H0. now destruct H0. reflexivity. + intros alpha _; eright. esplit. intro; subst. apply H. now rewrite gnawS_zero. reflexivity. * apply IHs; auto. discriminate. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)