proposition: Lemma LT2 : forall alpha alpha' n n' beta beta', nf (cons alpha n beta) -> nf (cons alpha' n' beta') -> alpha t1< alpha' -> cons alpha n beta t1< cons alpha' n' beta'.
proof: Proof. repeat split; auto; apply head_lt; auto. 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)