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