[Agda] Bool P -> Dec P'

[Sergei Meshveliani]

Please, how to write this via `case' ?

This is the conversion of a Boolean predicate to the decidable one:

----------------------------------------------------------------------
open import Data.Unit         using (⊤)
open import Data.Bool as Bool using (Bool; true; false; T)

boolP→Dec : ∀ {α} {A : Set α} → (P : A → Bool) → let P' : A → Set
                                                     P' = T ∘ P
                                                 in  Decidable P'
boolP→Dec P x  with  P x 
...          | true  = yes ⊤.tt                  
...          | false = no λ()  
----------------------------------------------------------------------

How to rewrite this via `case', so that it is type-checked ?
(in development Agda of November 2013).

Thanks,

------
Sergei