no goals
α : Type u_1
β : Type ?u.33481
is ts : List α
⊢ permutations (is ++ ts) = map (fun x => x ++ ts) (permutations is) ++ permutationsAux ts (reverse is)
simp [permutations, permutationsAux_append]