fact: Fixpoint subst_rest vars sigma : substitution := match sigma with | nil => nil | (x,u) :: sigma => if mem_bool eq_var_bool x vars then (x,u) :: (subst_rest vars sigma) else subst_rest vars sigma end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)