case mk
α : Type u_1
l : List α
⊢ ofFn (get { val := l, property := (_ : List.length l = List.length l) }) =
    { val := l, property := (_ : List.length l = List.length l) }
n : ℕ
α : Type u_1
v : Vector α n
⊢ ofFn (get v) = v
rcases v with ⟨l, rfl⟩
case mk.a
α : Type u_1
l : List α
⊢ toList (ofFn (get { val := l, property := (_ : List.length l = List.length l) })) =
    toList { val := l, property := (_ : List.length l = List.length l) }
case mk
α : Type u_1
l : List α
⊢ ofFn (get { val := l, property := (_ : List.length l = List.length l) }) =
    { val := l, property := (_ : List.length l = List.length l) }
apply toList_injective
case mk.a
α : Type u_1
l : List α
⊢ toList (ofFn (get { val := l, property := (_ : List.length l = List.length l) })) = l
case mk.a
α : Type u_1
l : List α
⊢ toList (ofFn (get { val := l, property := (_ : List.length l = List.length l) })) =
    toList { val := l, property := (_ : List.length l = List.length l) }
dsimp
no goals
case mk.a
α : Type u_1
l : List α
⊢ toList (ofFn (get { val := l, property := (_ : List.length l = List.length l) })) = l
simpa only [toList_ofFn] using List.ofFn_get _