[Agda] isHead x (x :: xs)

[Sergei Meshveliani]

Please, how to prove the following?

  isHead : ℕ → List ℕ → Bool
  isHead _ []        = false 
  isHead x (y ∷ ys)  with  x ≟ y
  ...              | yes _ = true 
  ...              | no _  = false 

  isHP : (x : ℕ) → (xs : List ℕ) → isHead x (x ∷ xs) ≡ true
  isHP x xs =
              ??

Thanks,

------
Sergei