fact: Definition well_formed_cf_subst sigma := forall v, match find X.eq_bool v sigma with | None => True | Some t => well_formed_cf t end.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)