proposition: Lemma path_to_LT beta s alpha : path_to beta s alpha -> nf alpha -> beta t1< alpha.
proof: Proof. intro H; assert (H0 := path_to_not_In_zero H). rewrite path_to_path_toS_iff in H. intro; eapply path_toS_LT; eauto. auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)