fact: Parameter subst_comp_is_subst_comp : forall sigma1 sigma2 t, apply_subst (subst_comp sigma1 sigma2) t = apply_subst sigma1 (apply_subst sigma2 t).
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)