[Agda] list head eq

[Sergei Meshveliani]

Please, what is wrong here?
(Agda 2.5.1, ghc-7.10.2)

--------------------------------------------------------------------
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Nat     using (ℕ)
open import Data.List    using (List; []; _∷_; map)
open import Data.Product using (_×_; proj₁; _,_)

postulate  g : (x y : ℕ) → x ≡ y → ℕ

f : List (ℕ × ℕ) → ℕ
f ps  with  ps | map proj₁ ps

... | ((x , _) ∷ ps') | .x ∷ _ =  g x x PE.refl	   -- .x  ?
... | _               | _      =  0

f2 : List (ℕ × ℕ) → ℕ
f2 ps  with ps | map proj₁ ps

... | ((x , _) ∷ ps') | y ∷ _ =  g x y x≡y
                                     where
                                     x≡y : x ≡ y
                                     x≡y = PE.refl   -- ?? 
... | _               | _     =  0
------------------------------------------------------------------


Why ".x"  is rejected in  f ?

If  (x , _) is the head of  ps  and  y  the head of (map proj₁ ps), 
then  x  is identical to  y.  How to explain this to Agda  in terms of
patterns, like above?

Thanks,

------
Sergei