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