proposition: Lemma flatten_build_cons : forall f t l, arity f = AC -> well_formed_cf (Term f (t :: l)) -> permut (flatten f ((build f l) :: nil)) l.
proof: Proof. intros f t l Af W; apply flatten_build; trivial. intros; apply (well_formed_cf_alien Af W); 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)