proposition: Lemma size3_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 t_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 (Term f l))); case (Nat.eqb (size t) (size (Term f l))); [intro t_eq_fl | intro t_lt_fl]. absurd (size (Term f l) < size (Term f l)); auto with arith; generalize (size_direct_subterm t (Term f l) t_in_l); rewrite t_eq_fl; trivial. apply (size_direct_subterm t (Term f l) t_in_l). 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)