proposition: Lemma ac_size_build_lt : forall f l1 l2 t1, arity f = AC -> well_formed_cf (Term f (l1 ++ t1 :: l2)) -> ac_size (build f (l1 ++ l2)) < ac_size (Term f (l1 ++ t1 :: l2)).
proof: Proof. intros f l1 l2 t1 Ar W. apply Nat.lt_le_trans with (ac_size (build f (l1 ++ l2)) + ac_size t1). rewrite (plus_n_O (ac_size (build f (l1 ++ l2)))); rewrite <- Nat.add_assoc; apply Nat.add_lt_mono_l; simpl; unfold lt; apply ac_size_ge_one; elim (well_formed_cf_unfold _ W); intros Wl _; apply Wl; apply in_or_app; right; left; trivial. apply Nat.lt_le_incl; apply ac_size_build_lt_args; trivial. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching)