n : ℕ
α : Type u_1
v : Vector α 1
⊢ toList (head v ::ᵥ tail v) = [head (head v ::ᵥ tail v)]
n : ℕ
α : Type u_1
v : Vector α 1
⊢ toList v = [head v]
rw [← v.cons_head_tail]
no goals
n : ℕ
α : Type u_1
v : Vector α 1
⊢ toList (head v ::ᵥ tail v) = [head (head v ::ᵥ tail v)]
simp only [toList_cons, toList_nil, head_cons, eq_self_iff_true, and_self_iff, singleton_tail]