[Agda] `with' -> `case' example

[Sergei Meshveliani]

Please, how to rewrite the below `with' in  keys-commute-delByKey
to `case' ?
The `with' variant is type-checked (in Agda-2.4.2), the `case' one does
not.

Thanks,

------
Sergei



**********************************************************************
open import Function using (_∘_; case_of_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Unary   using (Decidable)
open import Relation.Binary  using (module Setoid; module DecSetoid; 
                                                          DecSetoid)
                             renaming (Decidable to Decidable₂)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≗_)
open import Data.Product using (_×_; proj₁; _,_)
open import Data.List    using (List; []; _∷_; map)


----------------------------------------------------------------------
delBy : ∀ {α p} {A : Set α} {P : A → Set p} →
                            (P? : Decidable P) → List A → List A
delBy _  []       = []
delBy P? (x ∷ xs) = case P? x of \ { (yes _) → xs
                                   ; (no _)  → x ∷ (delBy P? xs) }

----------------------------------------------------------------------
module AssocList-pack {α α= β} (Key : DecSetoid α α=) (Val : Set β)
  where
  open DecSetoid Key using (_≈_; _≟_) renaming (Carrier to K)
  KV = K × Val

  del : K → List K → List K
  del x =  delBy (_≟_ x)

  getKeys : List KV → List K
  getKeys = map proj₁

  delByKey : K → List KV → List KV
  delByKey k =  delBy ((_≟_ k) ∘ proj₁)

  keys-commute-delByKey : 
                        {k : K} → getKeys ∘ delByKey k ≗ del k ∘ getKeys
  keys-commute-delByKey {k} []              =  PE.refl
  keys-commute-delByKey {k} ((k' , v) ∷ ps) =
    case
        k ≟ k'
    of \ 
    { (yes _) → PE.refl                                                
    ; (no _)  → PE.cong (_∷_ k') (keys-commute-delByKey {k} ps) }

{-  
    with k ≟ k'
  ...                         
      | yes _ = PE.refl                                                
  ... | no _  = PE.cong (_∷_ k') (keys-commute-delByKey {k} ps)
-}