proposition: Lemma acc_from_LT (alpha beta : T1) : acc_from alpha beta -> nf alpha -> beta t1< alpha.
proof: Proof. destruct 1 as [s Hs]; intro; eapply path_to_LT; eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)