fact: Parameter subst_rest_ok : forall vars sigma v, In v vars -> apply_subst (subst_rest vars sigma) (Var v) = apply_subst sigma (Var v).
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)