ι : Type ?u.233879
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
⊢ reverse (foldr (fun h t => h :: t) [] (reverse l)) = l
ι : Type ?u.233879
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
⊢ reverse (foldl (fun t h => h :: t) [] l) = l
rw [← foldr_reverse]
no goals
ι : Type ?u.233879
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
⊢ reverse (foldr (fun h t => h :: t) [] (reverse l)) = l
simp only [foldr_self_append, append_nil, reverse_reverse]