intro L hL 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, ⋯⟩
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 τ
hL : L = ofFn f
hi' : i < L.length
⊢ get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩