[GOAL]
α : Type v
inst✝ : Small.{u, v} α
⊢ Small.{u, v} (List α)
[PROOFSTEP]
let e : (Σ n, Vector α n) ≃ List α := Equiv.sigmaFiberEquiv List.length
[GOAL]
α : Type v
inst✝ : Small.{u, v} α
e : (n : ℕ) × Vector α n ≃ List α := Equiv.sigmaFiberEquiv List.length
⊢ Small.{u, v} (List α)
[PROOFSTEP]
exact small_of_surjective e.surjective
