proposition: Lemma well_formed_cf_build_cons : forall f t l, arity f = AC -> well_formed_cf (Term f (t :: l)) -> well_formed_cf (build f l).
proof: Proof. intros f t l Af W; apply well_formed_cf_build; trivial. apply le_S_n; replace (S (length l)) with (length (t :: l)); trivial; apply well_formed_cf_length with f; trivial. intros; apply (well_formed_cf_subterms W); right; 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)