v : Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => y) (Vector.head v) = Nat.pred (Vector.head v)
v : Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => Vector.head (y ::ᵥ IH ::ᵥ v)) (Vector.head v) = Nat.pred (Vector.head v)
simp
no goals
v : Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH => y) (Vector.head v) = Nat.pred (Vector.head v)
cases v.head <;> rfl