[Agda] Decidable _\~~_ of Semiring

[Serge D. Mechveliani]

On Fri, Nov 09, 2012 at 01:40:06PM +0100, Andreas Abel wrote:
> There are two different definitions of Decidable:
>
> 1) The one in Relation.Unary is for predicates (unary relations).
> 2) The one in Relation.Binary is for binary relations.
>
> Just import the right one and the type error goes away.
> [..]

I do not see in  Relation.Binary  of lib-0.6  any declaration of the  
Decidable  type. Neither `data' nor `record' nor as a function. 

On the other hand  
                  open import Relation.Binary using ( Decidable )
does help
-- !?
How can this import work? 

Thanks,

------
Sergei