[Agda] Decidable _\~~_ of Semiring

[Serge D. Mechveliani]

On Fri, Nov 09, 2012 at 09:07:36AM -0500, Daniel Peebles wrote:
> It's in Relation.Binary.Core, which is imported and then opened publicly at
> the top of the file.
> 

  module Relation.Binary where
  ...
  open import Relation.Binary.Core as Core using (_\equiv_)
  import Relation.Binary.Indexed.Core as I

  ----------------------------------------------------------------------
  -- Simple properties and equivalence relations

  open Core public hiding (_\equiv_; refl; ...) 
  ...


This combination of  Core using (_\equiv_)
and                  open Core public hiding (_\equiv_; refl; ...) 
is some feature!
(difficult to understand).

It is sometimes very difficult to find out from where to import a library 
thing. 
I do not know, may be import in  lib  can be set in a more plain way.

Thanks,

------
Sergei