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