case mk
n : ℕ
α : Type u_1
val✝ : List α
property✝ : List.length val✝ = n
⊢ reverse (reverse { val := val✝, property := property✝ }) = { val := val✝, property := property✝ }
n : ℕ
α : Type u_1
v : Vector α n
⊢ reverse (reverse v) = v
cases v
no goals
case mk
n : ℕ
α : Type u_1
val✝ : List α
property✝ : List.length val✝ = n
⊢ reverse (reverse { val := val✝, property := property✝ }) = { val := val✝, property := property✝ }
simp [Vector.reverse]