no goals
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (permutations' ts) = permutations' (map f ts)
induction' ts with t ts ih <;> [rfl; simp [← ih, map_bind, ← map_map_permutations'Aux, bind_map]]