case mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
val✝ : List α
property✝ : List.length val✝ = m
⊢ toList (drop n { val := val✝, property := property✝ }) = List.drop n (toList { val := val✝, property := property✝ })
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
v : Vector α m
⊢ toList (drop n v) = List.drop n (toList v)
cases v
no goals
case mk
α : Type u
β : Type v
φ : Type w
n✝ n m : ℕ
val✝ : List α
property✝ : List.length val✝ = m
⊢ toList (drop n { val := val✝, property := property✝ }) = List.drop n (toList { val := val✝, property := property✝ })
rfl