proposition: Lemma size3_lex3_prec : forall u f g h l l' s, In u l -> prec_eq Prec g h -> o_size3 (s,(Term g l',u)) (s,(Term h l',Term f l)).
proof: Proof. intros u f g h l l' s 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 (Term g l')) (size (Term h l'))); case (Nat.eqb (size (Term g l')) (size (Term h l'))); [intros _ | intro t_diff_t]. intros. apply (size_direct_subterm u (Term f l) u_in_l). intros. 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)