Proof that Vec ++ [] == Vec?

Is there a handy proof that:

++[] : ∀ {ℓ} {A : Set ℓ} {n} (vec : Vec A n) -> vec ++ [] ≡ vec

I am unable to even write the type of this proof, apparently, because

n != n Nat.+ Nat.zero of type ℕ
when checking that the expression vec has type
Vec A (n Nat.+ Nat.zero)