English
If you build a list by repeatedly prepending the current element using foldl (t,h) -> h :: t starting with [], then reversing the result yields the original list: reverse (foldl (fun t h => h :: t) [] l) = l.
Русский
Если построить список слева, последовательно добавляя элементы слева через foldl (t,h) → h :: t, начиная с [], то обращение полученного списка возвращает исходный список: reverse (foldl (λ t h. h :: t) [] l) = l.
LaTeX
$$$$\operatorname{reverse}(\operatorname{foldl}(\lambda t\, h. h:\, t)\, []\, l) = l.$$$$
Lean4
theorem reverse_foldl {l : List α} : reverse (foldl (fun t h => h :: t) [] l) = l := by simp