[Agda] StrictLex in library

[Sergei Meshveliani]

People,

I look into  Relation.Binary.List.StrictLex

of Standard library (of April 13, 2017)

and see that it is for  (List A)  for  A : Set.

What is the reason for restricting  A  to Set of the level  zero ?

I need an implementation for StrictTotalOrder for List A,  where
A has StrictTotalOrder for _<_,  and  A : Set a,  a : Level.

Need I to modify  Relation.Binary.List.StrictLex
by replacing  Set  with  (Set a) ?

Can anyone advise, please?

------
Sergei