no goals
ι : Type ?u.27240
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
f : α → β
l₁ l₂ : List α
⊢ map f (reverseAux l₁ l₂) = reverseAux (map f l₁) (map f l₂)
simp only [reverseAux_eq, map_append, map_reverse]