[Agda] lists as sets

[Sergei Meshveliani]

People,

For  A : Setoid α α=,  I define

  C = Setoid.Carrier A
  open Membership A using (_∈_; _⊆_)

  _=set_ : Rel (List C) (α ⊔ α=)
  xs =set ys =  xs ⊆ ys × ys ⊆ xs

And then need to have the list setoid by the _=set_ equality
(not the one of Pointwise). This will be actually a finite set setoid.
Has Standard library something ready for this?

Thanks,

------
Sergei