proposition: Lemma LT_path_to (alpha beta : T1) : beta t1< alpha -> {s : list nat | path_to beta s alpha}.
proof: Proof. intro H; destruct (LT_path_toS H) as [s Hs]; exists (shift s); now rewrite <- path_toS_path_to. Defined.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)