proposition: Remark R24 : const_pathS (n+l) gamma beta -> beta t1<= delta.
proof: Proof. intro H; destruct (R23 H). - rewrite <- e; apply LE_refl. eapply LT_nf_r; eauto. - apply LE_r;auto. eapply const_pathS_LT;eauto. + unfold delta; apply nf_canon. unfold gamma; apply standard_gnaw_nf;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)