suffices ∀ L (_h : L = ofFn f) (hi' : i < L.length),
  get L ⟨i,hi'⟩ = f ⟨i, size_ofFn (C := C) f ▸ hi⟩
  from this _ (toList_ofFn _) (by simp at hi; simp [List.instSeqList, *])
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ get (toList (ofFn f)) (Fin.cast ⋯ ⟨i, hi⟩) = f (Fin.cast ⋯ ⟨i, hi⟩)
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ ∀ (L : List τ), L = ofFn f → ∀ (hi' : i < L.length), get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩