proposition: Lemma size3_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 u_in_l; unfold o_size3, size3, size2, lex; generalize (beq_nat_ok (size s) (size s)); case (Nat.eqb (size s) (size s)); [intros _ | intro s_diff_s]. generalize (beq_nat_ok (size t) (size t)); case (Nat.eqb (size t) (size t)); [intros _ | intro t_diff_t]. apply (size_direct_subterm u (Term f l) u_in_l). apply False_rect; apply t_diff_t; reflexivity. apply False_rect; apply s_diff_s; reflexivity. Defined.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)