fact: Fixpoint apply_cf_subst (sigma : substitution) (t : term) {struct t} : term := match t with | Var v => match find X.eq_bool v sigma with | None => t | Some v_sigma => v_sigma end | Term f l => let l_sigma := match arity f with | AC => quicksort (flatten f (map (apply_cf_subst sigma) l)) | C => quicksort (map (apply_cf_subst sigma) l) | Free _ => map (apply_cf_subst sigma) l end in Term f l_sigma end.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)