proposition: Lemma const_pathS_LE i : forall alpha beta, nf alpha -> const_path (S i) alpha beta -> beta t1<= alpha.
proof: Proof. intros; apply LE_r; eapply const_pathS_LT; eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)