[Agda] with -> case example

[Sergei Meshveliani]

Please, how to rewrite this to `case' ?


filterStep : ∀ {α} {A : Set α}
             (p : A → Bool) → (x : A) → p x ≡ true → (xs : List A) →
                                   filter p (x ∷ xs) ≡ x ∷ (filter p xs)
filterStep p x px=T xs
                       with  p x | px=T
...                  | .true | PE.refl = PE.refl 


-------------------------------------------------------------------------
filterStep p x px=T xs =  case (p x , px=T)  of \     
                                         { (.true , PE.refl) → PE.refl }
" p x != true of type Bool
  when checking that the expression px=T has type true ≡ true
"

Thanks,

------
Sergei