# [Agda] again `with' vs `case'

Sergei Meshveliani mechvel at botik.ru
Mon Aug 26 20:35:35 CEST 2013

```People,
there is again a strange point about `case' :
a proof  cong2-∈  for the congruence of  Membership._∈_  by the list
argument
(for  lib-0.7,  Agda of darcs August 2013).

--------------------------------------------------------------------------
open import Level           using (Level)
open import Function        using (case_of_)
open import Relation.Binary using (Setoid; module Setoid)
open import Data.List       using (List; []; _∷_)
open import Data.List.Any using (Any; module Any; module Membership)
open import Relation.Binary.List.Pointwise as ListPoint using ()
renaming (_∷_ to _∷p_)

cong2-∈ : ∀ {c l} {A : Setoid c l} →
let open Setoid A using (_≈_) renaming (Carrier to C)
_∈_  = Membership._∈_ A
_=l_ = Setoid._≈_ (ListPoint.setoid A)
in
(x : C) → (xs ys : List C) → xs =l ys → x ∈ xs → x ∈ ys

open Any
cong2-∈ {A = A} x (u ∷ _)  (v ∷ _)  (u=v ∷p =tail) (here x=u) =
here x=v
where
open Setoid A
x=v : x ≈ v
x=v = trans x=u u=v

cong2-∈ {A = A} x (u ∷ xs) (v ∷ ys) (u=v ∷p =tail) (there x∈xs) =
there (cong2-∈ x xs ys =tail x∈xs)

{- -------------
cong2-∈ {A = A} x (u ∷ xs) (v ∷ ys) (u=v ∷p =tail) x∈u-xs =
case x∈u-xs of \
{
(here x=u)   → let x=v : x ≈ v
x=v = trans x=u u=v
in  here x=v

; (there x∈xs) → there (cong2-∈ x xs ys =tail x∈xs)
}
where
open Setoid A
---------------------
-}
-----------------------------------------------------------------------------

* It is type-checked,
* the `case' variant repeats everything, and is not type-checked:

"Missing cases:  cong2-∈ {_} {_} {_} _ ._ ._ ListPoint.[] _ "

If it rejects  ListPoint.[]  in the first variant, why does it need it
in the `case' variant?

Thanks,

------
Sergei

```