case nil
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
start : ℕ
⊢ foldrIdx f b [] start = foldrIdxSpec f b [] start

case cons
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (start : ℕ), foldrIdx f b tail✝ start = foldrIdxSpec f b tail✝ start
start : ℕ
⊢ foldrIdx f b (head✝ :: tail✝) start = foldrIdxSpec f b (head✝ :: tail✝) start
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
as : List α
start : ℕ
⊢ foldrIdx f b as start = foldrIdxSpec f b as start
induction as generalizing start
no goals
case nil
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
start : ℕ
⊢ foldrIdx f b [] start = foldrIdxSpec f b [] start
rfl
no goals
case cons
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (start : ℕ), foldrIdx f b tail✝ start = foldrIdxSpec f b tail✝ start
start : ℕ
⊢ foldrIdx f b (head✝ :: tail✝) start = foldrIdxSpec f b (head✝ :: tail✝) start
simp only [foldrIdx, foldrIdxSpec_cons, *]