[Agda] import in st.library

[Sergei Meshveliani]

People,
Has sense to use more `using' in the Standard library modules?
It is often difficult to find the origin of the imported items.
For example:
--------------------------------------------------------------
module Relation.Binary.PropositionalEquality where
...
open import Relation.Binary
import Relation.Binary.Indexed as I
open import Relation.Binary.Consequences
...
open import Relation.Binary.PropositionalEquality.Core public
... 
setoid : ∀ {a} → Set a → Setoid _ _
setoid A = record
  { Carrier       = A
  ; _≈_           = _≡_
  ; isEquivalence = isEquivalence
  }  
--------------------------------------------------------------------

Where this  isEquivalence  is imported from? I need to inspect 4
candidate modules. There are many other examples. 
There is some trick with the agda-mode-emacs for finding a definition 
(I do not recall how to). 
But probably `using' makes it easier.

Regards,

------
Sergei