[Agda] struggling `with'

[Sergei Meshveliani]

People,
After two days struggle against `with' in my example, I find the
following way out: 

 ---------------------------------------------------------
 foo ... =  prove (k ≟ k')
   where
   ...   
   case≈ : k ≈ k' → 
               ins kv (ins ku (k'w ∷ ps)) =pn ins (k , ckvu) (k'w ∷ ps)
   case≈ k≈k' =
      begin-pn
        ins kv (ins ku (k'w ∷ ps))   =pn[ =pn-reflexive $ 
                                          PE.cong (ins kv) e1 ]
        ins kv ((k' , ckuw) ∷ ps)    =pn[ =pn-reflexive e2 ]
        (k' , comb k v ckuw) ∷ ps    =pn[ e0 ∷pn =pn-refl ]
        (k' , comb k ckvu w) ∷ ps    =pn[ =pn-reflexive $ PE.sym e3 ]
        ins (k , ckvu) (k'w ∷ ps)
      end-pn
      where
      e0 : (k' , comb k v ckuw) =p (k' , comb k ckvu w)
      e0 = (≈refl , sym-assoc-comb)

      e1 :  ins ku ((k' , w) ∷ ps) ≡ (k' , ckuw) ∷ ps
      e1 with k ≟ k'
      ... | yes _   = PE.refl
      ... | no k≉k' = ⊥-elim $ k≉k' k≈k'

      e2 :  ins kv ((k' , ckuw) ∷ ps) ≡ (k' , comb k v ckuw) ∷ ps
      e2 with k ≟ k'
      ... | yes _   = PE.refl
      ... | no k≉k' = ⊥-elim $ k≉k' k≈k'

      e3 :  k'w ∷ (ins (k , ckvu) ps) ≡ ins (k , ckvu) (k'w ∷ ps)
      e3 with k ≟ k'
      ... | no _     = PE.refl
      ... | yes k≈k' = ⊥-elim $ k≉k' k≈k'

   ------------------------------------------------
   case≉ : ¬ k ≈ k' →
           ins kv (ins ku (k'w ∷ ps))  =pn  ins (k , ckvu) (k'w ∷ ps)
   case≉ k≉k' = ...
                -- a similar junk

   ------------------------------------------------
   prove : Dec (k ≈ k') → ins kv (ins ku (k'w ∷ ps)) =pn 
                          ins (k , comb k v u) (k'w ∷ ps)
   prove (no k≉k')  = case≉ k≉k'
   prove (yes k≈k') = case≈ k≈k'
 ----------------------------------------------------------------------


The code is type-checked, but looks ugly.
For example,  e1, e2, e3  have the same implementation
(each of them stupidly asking "k ≟ k'" despite that k≈k' is ready).

I expected that  "with k ≟ k'"  needs to be asked not more than once in
case≈. But I fail to arrange this.
For example, 

   e00 :  ins kv (ins ku (k'w ∷ ps)) ≡ (k' , comb k v ckuw) ∷ ps
   e00  with k ≟ k'                               
   ... | yes _   = PE.refl                  
   ... | no k≉k' = ⊥-elim $ k≉k' k≈k' 

presents the two steps of normalization for `ins' ('ins' is applied
twice in the LHS, and its implmentation asks "k ≟ k'"), 
and the value  (k' , comb k v ckuw) ∷ ps  
is the normal form.

But Agda-2.4.2.2 does not see this, and rejects this proof. 
To prove e00, I need to split it to the two equations, and to apply
"with k ≟ k'"  for each equation.

Can the goal be written in a nicer way?

Thanks,

------
Sergei