proposition: Lemma path_toS_LT beta s alpha: path_toS beta s alpha -> nf alpha -> beta t1< alpha.
proof: Proof. induction 1. destruct H. intro; subst; now apply canonS_LT. intro; apply LT_trans with gamma; auto. apply IHpath_toS. destruct H;subst. now apply nf_canon. destruct H. subst; apply canonS_LT; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)