case nil
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
start : ℕ
⊢ foldlIdx f a [] start = foldlIdxSpec f a [] start

case cons
α : Type u
β : Type v
f : ℕ → α → β → α
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (a : α) (start : ℕ), foldlIdx f a tail✝ start = foldlIdxSpec f a tail✝ start
a : α
start : ℕ
⊢ foldlIdx f a (head✝ :: tail✝) start = foldlIdxSpec f a (head✝ :: tail✝) start
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
bs : List β
start : ℕ
⊢ foldlIdx f a bs start = foldlIdxSpec f a bs start
induction bs generalizing start a
no goals
case nil
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
start : ℕ
⊢ foldlIdx f a [] start = foldlIdxSpec f a [] start
rfl
no goals
case cons
α : Type u
β : Type v
f : ℕ → α → β → α
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (a : α) (start : ℕ), foldlIdx f a tail✝ start = foldlIdxSpec f a tail✝ start
a : α
start : ℕ
⊢ foldlIdx f a (head✝ :: tail✝) start = foldlIdxSpec f a (head✝ :: tail✝) start
simp [foldlIdxSpec, *]