[Agda] Setoid for List

[Serge D. Mechveliani]

People, 
why the standard library  lib-0.6  does not provide  Setoid and DecSetoid  
instances for  List ?
(does it?)
If it does not, then is the following a reasonable program for this?

  listSetoid : {c l : Level} -> DecSetoid c l -> Setoid _ _
  listSetoid A = record{ Carrier       = List ACarr 
                       ; _\~~_         = eqList               
                       ; isEquivalence = isEquiv } 
      where    
      ACarr = DecSetoid.Carrier A                                   
      open DecSetoid {{...}}                                         
      eqList : Rel (List ACarr) _                                       
      eqList []        []        = \top                          
      eqList []        (_ :: _)  = \bot                                   
      eqList (_ :: _)  []        = \bot                                 
      eqList (x :: xs) (y :: ys)  with x \?= y                            
      ...                       | yes _ = eqList xs ys                    
      ...                       | _     = \bot
                                                                              
      isEquiv : IsEquivalence eqList            
      isEquiv =  <a proof, which I would have to set if not find in 
                  libraries>

(I use here `\' for the math symbols).

Thanks,

------
Sergei