case nil
α : Type u
β : Type v
f : α → α
a✝ a : α
⊢ foldl (fun b x => f b) a [] = (f^[length []]) a

case cons
α : Type u
β : Type v
f : α → α
a✝ : α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x => f b) a l = (f^[length l]) a
a : α
⊢ foldl (fun b x => f b) a (b :: l) = (f^[length (b :: l)]) a
α : Type u
β : Type v
f : α → α
a : α
l : List β
⊢ foldl (fun b x => f b) a l = (f^[length l]) a
induction' l with b l H generalizing a
no goals
case nil
α : Type u
β : Type v
f : α → α
a✝ a : α
⊢ foldl (fun b x => f b) a [] = (f^[length []]) a
rfl
no goals
case cons
α : Type u
β : Type v
f : α → α
a✝ : α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x => f b) a l = (f^[length l]) a
a : α
⊢ foldl (fun b x => f b) a (b :: l) = (f^[length (b :: l)]) a
rw [length_cons, foldl, iterate_succ_apply, H]