[Agda] again `with' vs `case'

[Sergei Meshveliani]

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