no goals
α : Type u_1
β : Type ?u.363665
γ : Type ?u.363668
σ : Type ?u.363671
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
x✝ : Vector α n
l : List α
h : List.length l = n
⊢ List.tail (Vector.toList { val := l, property := h }) = Vector.toList (Vector.tail { val := l, property := h })
cases l <;> rfl