Vectors whose underlying list is a cons

A vector of length n + 1 has underlying list a :: l exactly when its head is a and the underlying list of its tail is l (List.Vector.toList_eq_cons_iff).

theorem List.Vector.toList_eq_cons_iff {α : Type u_1} {n : ℕ} {v : Vector α (n + 1)} {a : α} {l : List α} : v.toList = a :: l ↔ v.head = a ∧ v.tail.toList = l

The underlying list of a nonempty vector is a :: l iff its head is a and its tail has underlying list l.