proposition: Lemma flatten_build_inside : forall f t l1 l2, arity f = AC -> well_formed_cf (Term f (l1 ++ t :: l2)) -> permut (flatten f ((build f (l1 ++ l2)) :: nil)) (l1 ++ l2).
proof: Proof. intros f t l1 l2 Af W; apply flatten_build; trivial. intros u In_u; apply (well_formed_cf_alien Af W); elim (in_app_or _ _ _ In_u); clear In_u; intro In_u; apply in_or_app; [left | right; right]; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)