v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.succ IH) (Vector.head v) =
    Vector.head v + Vector.head (Vector.tail v)
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.succ (Vector.head (Vector.tail (y ::ᵥ IH ::ᵥ Vector.tail v))))
      (Vector.head v) =
    Vector.head v + Vector.head (Vector.tail v)
simp
no goals
v : Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (Vector.head (Vector.tail v)) (fun y IH => Nat.succ IH) (Vector.head v) =
    Vector.head v + Vector.head (Vector.tail v)
induction v.head <;> simp [*, Nat.succ_add]