simp [List.instSeqList]
case mk.refl
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
hi' : i < (ofFn f).length
⊢ get (ofFn f) ⟨i, hi'⟩ = f ⟨i, ⋯⟩
no goals