[Agda] reasoning combinator names

[Sergei Meshveliani]

People,

I have  Foo.agda  where it is needed reasoning by combinators of
standard-library-master for _≡_ and _≤_ for different types, as follows.
 
* reasoning with _≡_ on ℕ and FooData,  
* reasoning with _≤_ on ℕ.  

I usually agree such reasonings by renaming some of the reasoning
combinators.
But this time such renaming is forbidden. 
What reasoning modules to import, what to substitute?

Thanks,

------
Sergei