no goals
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r ys f).snd = map (fun x => f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]