simp only [mapIdx'_cons, length, IH]
α : Type u
β : Type v
γ : Type w
as✝ : List α
f✝ : Fin (length as✝) → α → β
a : α
as : List α
IH : ∀ (x : Fin (length as) → α → β), length (mapIdx' as x) = length as
f : Fin (length (a :: as)) → α → β
⊢ length (mapIdx' (a :: as) f) = length (a :: as)
no goals