[Agda] with vs case example

[Sergei Meshveliani]

Please,

how to change the below `with' to `case' ? 


 foo : a ∣ 1# → (null pItems ≡ true)
 foo a∣1
         with pItems
 ... | []       =  PE.refl
 ... | item ∷ _ =  ⊥-elim $ a∤1 a∣1
                   where
                   postulate a∤1 : a ∤ 1#

 {- variant 
 foo a∣1 =  case pItems of \ { []         → PE.refl 
                             ; (item ∷ _) → let a∤1 : a ∤ 1#
                                                a∤1 = anything 
                                            in  ⊥-elim $ a∤1 a∣1     
                             } 
 }

`with' is type-checked, and `case' is not.

Thanks,

------
Sergei