case nil
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ f : ℕ → α → β
⊢ length (mapIdx f []) = length []

case cons
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ : ℕ → α → β
hd : α
tl : List α
IH : ∀ (f : ℕ → α → β), length (mapIdx f tl) = length tl
f : ℕ → α → β
⊢ length (mapIdx f (hd :: tl)) = length (hd :: tl)
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
⊢ length (mapIdx f l) = length l
induction' l with hd tl IH generalizing f
no goals
case nil
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ f : ℕ → α → β
⊢ length (mapIdx f []) = length []
rfl
no goals
case cons
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ : ℕ → α → β
hd : α
tl : List α
IH : ∀ (f : ℕ → α → β), length (mapIdx f tl) = length tl
f : ℕ → α → β
⊢ length (mapIdx f (hd :: tl)) = length (hd :: tl)
simp [IH]