proposition: Lemma LT_acc_from (alpha beta : T1) : beta t1< alpha -> acc_from alpha beta.
proof: Proof. intro H; destruct (LT_path_toS H); apply path_acc_from with (map S x). now apply path_toS_path_to. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)