[Agda] with -> case example

[Sergei Meshveliani]

People,

I implement  deletion  del  from a list  (by _≈_, _≟_)
and the property  ∈del-x-xs-if  of membership by _≈_ to  del _≟_ x xs.

I have the questions:

1) what Standard library has for this?
2) how to rewrite  ∈del-x-xs-if  from `with' to `case' ? 

Thanks,

------
Sergei


--------------------------------------------------------------------
open import Level using (Level)
open import Function using (case_of_; case_return_of_)
open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Relation.Binary
                   using (module IsEquivalence; Setoid; module Setoid)
                   renaming (Decidable to Decidable₂)
open import Data.Empty using (⊥-elim)
open import Data.List  using (List; []; _∷_)
open import Data.List.Any using (Any; module Any; module Membership)

open Any

module Membership2 {α α= : Level} (A : Setoid α α=)
  where
  open Setoid A using (_≈_) renaming
                            (Carrier to C; isEquivalence to ≈equiv)
  open IsEquivalence ≈equiv using ()
                            renaming (sym to ≈sym; trans to ≈trans)
  open Membership A using (_∈_)


  del : (_≟_ : Decidable₂ _≈_) → C → List C → List C
  del _   _ []       =  []
  del _≟_ x (y ∷ xs) =  case x ≟ y of \ { (yes _) → xs
                                        ; (no _)  → y ∷ (del _≟_ x xs) }


  ∈del-x-xs-if : (_≟_ : Decidable₂ _≈_) → ∀ {x y xs} → ¬ x ≈ y → 
                                               y ∈ xs → y ∈ del _≟_ x xs
                                                                       
  ∈del-x-xs-if _≟_ {x} {_} {z ∷ _} x≉y (here y=z)  with x ≟ z
  ...                                                                           
      | yes x=z = ⊥-elim (x≉y (≈trans x=z (≈sym y=z)))
  ... | no _    = here y=z 
                          
  ∈del-x-xs-if _≟_ {x} {y} {z ∷ xs} x≉y (there y∈xs)  with x ≟ z   
  ...                                                       
      | yes _ = y∈xs  
  ... | no _  = there (∈del-x-xs-if _≟_ {x} {y} {xs} x≉y y∈xs)