[Agda] `case' vs `with'

[Sergei Meshveliani]

Dear Agda developers,

The below `case' version for `lemma' is not type-checked in Agda 2.5.2,
while the `with' version is type-checked.
  
I do not know of whether such `case' treating is intended in Agda, 
I report this for any occasion (because this difference looks strange).

Regards,

------
Sergei


-------------------------------------------------------------------
open import Function        using (case_of_)
open import Relation.Binary using (DecSetoid)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Relation.Nullary using (¬_; yes; no)
open import Data.Empty       using (⊥-elim)
open import Data.Product     using (_×_; _,_)
open import Data.List        using (List; []; _∷_)
                                     
module _ {α α=} (dS : DecSetoid α α=) (z : DecSetoid.Carrier dS)
  where
  open DecSetoid dS using (Carrier; _≈_; _≟_) 

  toList : Carrier → List Carrier
  toList x =  case x ≟ z of \ { (yes _) → []
                              ; (no _)  → (x ∷ [])
                              }

  lemma :  ∀ x → ¬ x ≈ z → (toList x) ≡ (x ∷ [])
  lemma x x≉z =   
              case x ≟ z of \ { (yes x≈z) → ⊥-elim (x≉z x≈z)
                              ; (no _)    → PE.refl
                              }
 {-
         with x ≟ z    
  ... | yes x≈z =  ⊥-elim (x≉z x≈z)
  ... | no _    =  PE.refl 
 -}
------------------------------------------------------------------