[Agda] with x =? x

[Sergei Meshveliani]

People,
I discover that Agda requires even  " with k ≟ k" :

  foo : .. -> ins (k , v) (ins (k , u) ps)  =pn  ins (k , comb k v u) ps

  foo {k} {u} {v} {[]}  with k ≟ k
  ...                 | yes _  =  =pn-refl          -- instance of  refl
  ...                 | no k≉k =  ⊥-elim $ k≉k ≈refl

_=pn_ is the pointwise equality for lists of certain pairs, when pairs
are compared by a certain _=p_.
ins  inserts a pair into a list "by the key". It compares  k ≟ k',  and
acts respectively.
And in  foo,   ins  is applied with   k for k'.

And a mere  " =pn-refl"  is not sufficient!
I have satisfied `ins' only with `with'.

This looks like a minor feature, but still:
is there a way to write nicer proofs than by using  "with x ≟ x"
?

Thanks,

------
Sergei