fact: Fixpoint apply_subst (sigma : substitution) (t : term) {struct t} : term := match t with | Var v => match find eq_var_bool v sigma with | None => t | Some v_sigma => v_sigma end | Term f l => Term f (map (apply_subst sigma) l) end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)