[Agda] two items in standard

[Sergei Meshveliani]

Dear all,

I have a question about Standard library
(is it better to ask them on GitHub for stdlib?).

I have two applications which can become proposals for Standard
library. And they use the 
                      InequalityReasoning 

module by Ulf Norell. 
May be, Standard could somehow include this InequalityReasoning ?

Regards,

------
Sergei