proposition: Lemma lex3 : forall u f l s t, In u l -> o_size3 (s,(t,u)) (s,(t,Term f l)).
proof: Proof. intros u f l s t In_u; unfold o_size3, size3, size2, lex; elim (eq_nat_dec (size s) (size s)); intro eq1. elim (eq_nat_dec (size t) (size t)); intro eq2. apply (size_direct_subterm u (Term f l) In_u). absurd (size t = size t); trivial. absurd (size s = size s); trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term