proposition: Lemma const_path_LT i : forall alpha beta, nf alpha -> const_path i alpha beta -> beta t1< alpha.
proof: Proof. destruct i as [| i]. - intros alpha beta H0 H1; inversion H1. - intros; apply const_pathS_LT with i; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)