[Agda] enigmatic `with'

[Sergei Meshveliani]

People,
I have 

  foo : ∀ k u v ps → ... → 
        ins (k , v) (ins (k , u) ps)  =pn  ins (k , comb k v u) ps

  foo k _ _ []    with k ≟ k
  ...                  | yes _  =  =pn-refl
  ...                  | no k≉k =  ⊥-elim $ k≉k ≈refl

  foo k u v ((k' , w) ∷ ps)  with k ≟ k'
  ...
      | no k≉k'  =  anything   -- so far
  ... | yes k≈k' =  e  
      where
      ...  -- a certain prelude
      ...
      e : ins (k , v) (ins (k , u) ((k' , w )∷ ps)) =pn
          ins (k , comb k v u) ((k' , w) ∷ ps)
      e =
        begin-pn
          ins kv (ins ku (k'w ∷ ps))    =pn[ =pn-reflexive e2 ]
          ins kv ((k' , ckuw) ∷ ps)     =pn[ =pn-reflexive e3 ]
          (k' , comb k v ckuw) ∷ ps     =pn[ e0 ∷pn =pn-refl ]
          (k' , comb k ckvu w) ∷ ps     =pn[ =pn-reflexive $ PE.sym e4 ]
          ins (k , ckvu) (k'w ∷ ps)
        end-pn

1) `e' itself is type-checked, 
2) the signature for  e  is exactly the one required in  foo,
3) Agda-2.4.2.2  reports of a wrong type for  e  in the branch 
   " yes k≈k' =  e".

Why Adga is so? What may be a way out?

Thanks,

------
Sergei