induction as generalizing i with
| nil => cases hi
| cons a as IH =>
  simp only [mapIdx'_cons]
  cases i with
  | zero => rfl
  | succ i => simp only [cons_getElem_succ, IH]; rfl
α : Type u
β : Type v
γ : Type w
as : List α
f : Fin (length as) → α → β
i : Nat
hi : i < length (mapIdx' as f)
⊢ (mapIdx' as f)[i] = f { val := i, isLt := (_ : i < length as) } as[i]
no goals