proposition: Lemma size2_lex2_bis_prec_eq : forall t f g P l s, prec_eq P f g -> o_size2 (s,Term f l) (s, Term g (t :: l)).
proof: Proof. intros a f g P l s f_eq_g; unfold o_size2, size2, lex; generalize (beq_nat_ok (size s) (size s)); case (Nat.eqb (size s) (size s)); [intros _ | intro s_diff_s]. do 2 rewrite size_unfold; apply Nat.add_lt_mono_l; simpl. exact (proj1 (Nat.add_lt_mono_r _ _ (list_size size l)) (size_ge_one a)). 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)