proposition: Lemma const_pathS_LT' (i : nat) (alpha beta : T1) (H:nf alpha): const_pathS i alpha beta -> alpha = zero \/ beta t1< alpha.
proof: Proof. intro H0; destruct (T1_eq_dec alpha zero). - now left. - right; eapply const_pathS_LT; eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)