added Membership to strandard library in Lists

src/Lists.lagda

@@ -879,6 +879,7 @@ Definitions similar to those in this chapter can be found in the standard librar
 import Data.List using (List; _++_; length; reverse; map; foldr; downFrom)
 import Data.List.All using (All; []; _∷_)
 import Data.List.Any using (Any; here; there)
+import Data.List.Any.Membership.Propositional using (_∈_)
 import Algebra.Structures using (IsMonoid)
 \end{code}
 The standard library version of `IsMonoid` differs from the

src/extra/Membership.agda

@@ -0,0 +1,15 @@
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.List using (List; []; _∷_; [_]; _++_)
+open import Data.List.Any using (Any; here; there)
+open import Data.List.Any.Membership.Propositional using (_∈_)
+open import Data.Nat using (ℕ)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+-- open import Data.List.Any.Membership.Propositional.Properties using (∈-++⁺ˡ; ∈-++⁺ʳ; ∈-++⁻)
+
+Id = ℕ
+
+_⊆_ : List Id → List Id → Set
+xs ⊆ ys = ∀ {w} → w ∈ xs → w ∈ ys
+
+lemma : ∀ {x : Id} → x ∈ [ x ]
+lemma = here refl