no goals
ι : Type ?u.239529
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a : α
l : List α
⊢ scanl f b (a :: l) = [b] ++ scanl f (f b a) l
simp only [scanl, eq_self_iff_true, singleton_append, and_self_iff]