proposition: Lemma lex1 : forall s f l t1 u1 t2 u2, In s l -> o_size3 (s,(t1,u1)) (Term f l,(t2,u2)).
proof: Proof. intros s f l t1 u1 t2 u2 In_s; unfold o_size3, size3, size2, lex; elim (eq_nat_dec (size s) (size (Term f l))). intro eq1; absurd (size (Term f l) < size (Term f l)); auto with arith; generalize (size_direct_subterm s (Term f l) In_s); rewrite eq1; trivial. intros; apply (size_direct_subterm s (Term f l) In_s). Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term