fact: Parameter subst_eq_vars : forall t sigma sigma', (forall v, In v (var_list t) -> apply_subst sigma (Var v) = apply_subst sigma' (Var v)) <-> apply_subst sigma t = apply_subst sigma' t.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)