proposition: Lemma LT4 : forall alpha n beta beta', nf (cons alpha n beta) -> nf (cons alpha n beta') -> beta t1< beta' -> cons alpha n beta t1< cons alpha n beta'.
proof: Proof. repeat split; auto; apply tail_lt. destruct H1; tauto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)