[Agda] Vec _ n cong by n

[Sergei Meshveliani]

Please, how to fix the following code?

  f : (xs : List ℕ) → (n : ℕ) → length xs ≡ n → Vec ℕ n
  f xs n |xs|=n =  v
                   where
                   v : Vec ℕ (length xs)
                   v = fromList xs

The type of  v  does not match.

According to  |xs|=n,  length xs  can be replaced with  n  in
Vec ℕ (length xs).
But probably,  cong  is not for  Vec  ...
So I wonder.

Thank you in advance for explanation,

------
Sergei