[Agda] " | condition " in report

[Sergei Meshveliani]

Please, 
what is wrong in the below program?

------------------------------------------------------------------------
open import Relation.Nullary using (yes; no)
open import Relation.Binary using
            (module Setoid; module DecSetoid; module DecTotalOrder)
open import Relation.Binary.PropositionalEquality as PE
                                                  using (_≡_; _≢_)
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
                                                       _∎ to _≡end)
open import Data.Empty      using (⊥-elim)
open import Data.Sum        using (_⊎_; inj₁; inj₂)
open import Data.Product    using (_×_; _,_; proj₁)
open import Data.Nat as Nat using (ℕ)
open import Data.List       using (List; []; _∷_; map)
open import Data.List.Any using (Any; module Any; module Membership)

open Any
natDecSetoid = DecTotalOrder.Eq.decSetoid Nat.decTotalOrder
_≟_          = DecSetoid._≟_    natDecSetoid
natSetoid    = DecSetoid.setoid natDecSetoid

open module Mem-ℕ = Membership natSetoid using (_∈_)

------------------------------------------------------------------------        
getKeys : List (ℕ × ℕ) → List ℕ
getKeys = map proj₁

insert : ℕ → ℕ → List (ℕ × ℕ) → List (ℕ × ℕ)
insert k v []               =  (k , v) ∷ []
insert k v ((k' , v') ∷ ps)  with  k ≟ k'
...                                | yes _ = (k' , v) ∷ ps
...                                | no _  = (k' , v') ∷ (insert k v ps)


lemma : (k v : ℕ) → (ps : List (ℕ × ℕ)) → let keys = getKeys ps
                                              ps'  = insert k v ps
                                          in
                                          k ∈ keys → getKeys ps' ≡ keys

lemma _ _ []               ()
lemma k _ ((k' , _) ∷ ps)  (here k=k')  with  k ≟ k'
...                                     | yes _   =  PE.refl
...                                     | no k≉k' =  ⊥-elim (k≉k' k=k')

lemma k v ((k' , v') ∷ ps) (there k∈ks)  with  k ≟ k'
... |
      yes k=k' =  PE.refl
... | no k≢k'  =  goal
        where
        ps'     = (k' , v') ∷ ps
        ins-ps' = insert k v ps'
        ks      = getKeys ps
        ins-ps  = insert k v ps

        keys-ins-ps'=k':keys-ins-ps :
                              getKeys ins-ps' ≡ k' ∷ (getKeys ins-ps)
        keys-ins-ps'=k':keys-ins-ps  with  k ≟ k'
        ...                         | no _     =  PE.refl
        ...                         | yes k=k' =  ⊥-elim (k≢k' k=k')

        goal : getKeys ins-ps' ≡ k' ∷ ks
               -- (map proj₁ (insert k v ((k' , v') ∷ ps)) ≡ k' ∷ ks)
        goal =
           ≡begin
             getKeys ins-ps'         ≡[ keys-ins-ps'=k':keys-ins-ps  ]
             k' ∷ (getKeys ins-ps)   ≡[ PE.cong (_∷_ k')
                                                (lemma k v ps k∈ks) ]
             k' ∷ ks
           ≡end
---------------------------------------------------------------------------


Development Agda of November ~20 2013 MAlonzo 

finds that everything is correct -- except that the last branch of 
      ... | no k≢k'  =

must have the goal type different to  getKeys ins-ps' ≡ k' ∷ ks
It reports
"
map (λ r → proj₁ r) (insert k v ((k' , v') ∷ ps) | k Nat.≟ k') !=
k' ∷ map (λ r → proj₁ r) (insert k v ps) of type List ℕ
when checking that the expression goal has type
map (λ r → proj₁ r) (insert k v ((k' , v') ∷ ps) | no k≢k') ≡
k' ∷ map (λ r → proj₁ r) ps
"

Normalizing the last type expression in the report gives
{-                                                                              
 map proj₁ (insert k v ((k' , v') ∷ ps) | no k≢k') ≡ 
                                                 k' ∷ map proj₁ ps
 -->
 getKeys (insert k v ps' | no k≢k')  ≡  k' ∷ getKeys ps
 -->
 getKeys (ins-ps' | no k≢k')  ≡  k' ∷ ks 
-}

It differs from the  `goal'  type only in adding   "| no k≢k' ".

1) I do not see what is wrong in my program.
2) How to fix?

Thank you in advance for explanation,

------
Sergei