fact: Parameter well_formed_cf_build : forall f l, arity f = AC -> 1 <= length l -> (forall t, In t l -> well_formed_cf t) -> (forall t, In t l -> match t with | Var _ => True | Term g _ => f <> g end) -> well_formed_cf (build f l).
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)