∀ {α : Type u_1} {β : Type u_2} {l' : List β} {l : List α} {f : (i : ℕ) → α → i < l.length → β},
  (l.mapFinIdx f = l') = ∃ (h : l'.length = l.length), ∀ (i : ℕ) (h_1 : i < l.length), l'[i] = f i l[i] h_1