proposition: Lemma lex_length : forall ss ts : list ES.A, lex ss ts -> length ss = length ts.
proof: Proof. induction ss as [ | s ss IHss]; intros ts Hlex. inversion Hlex; trivial. destruct ts as [ | t ts]; inversion Hlex; subst. simpl; auto with arith. simpl; gen (IHss ts H0); auto with arith. Qed.
imports: CoLoR(RelExtras ListUtil AccUtil LogicUtil)