proposition: Lemma path_toS_zero_inv x u alpha : path_toS zero (x::u) alpha -> {alpha = one /\ u = nil} + {u <> nil /\ path_toS one (but_last x u) alpha}.
proof: Proof. destruct u. - left;split; auto; eapply path_toS_zero_one; eauto. - right; split. + discriminate. + apply path_toS_zero_but_last; auto. discriminate. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)