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