English
If the scanl sequence is nonempty, its head equals the initial value b.
Русский
Если последовательность scanl непуста, её голова равна начальному значению b.
LaTeX
$$$$\forall f,b,l:\ (\text{Ne}(\operatorname{scanl} f b l, \varnothing))\;\Rightarrow\; (\operatorname{scanl} f b l).head(h) = b.$$$$
Lean4
@[simp]
theorem head_scanl (h : scanl f b l ≠ []) : (scanl f b l).head h = b := by cases l <;> simp