fact: Definition subst_comp sigma1 sigma2 := (map_subst (fun _ t => apply_subst sigma1 t) sigma2) ++ (map_subst (fun v t => match find eq_var_bool v sigma2 with | None => t | Some v_sigma2 => apply_subst sigma1 v_sigma2 end) sigma1).
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)