From 7273c6e06618ba3b284fc3e60490c2104f671a9c Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Wed, 25 Sep 2024 21:53:30 +0100
Subject: [PATCH] Lists: porting several lemmas from other libraries (#2479)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Lists: irrelevance of membership (in unique lists)

* Lists: the empty list is always a sublist of another

* Lists: lookupMaybe (unsafe version of lookup)

* List: `concatMap⁺` for the subset relation

* Lists: memberhsip lemma for AllPairs

* Lists: membership lemmas for map∘filter

* Lists: lemmas about concatMap

* Lists: lemmas about deduplicate

* Lists: membership lemmas about nested lists

* Lists: extra subset lemmas about _∷_

* Lists: extra lemmas about _∷_/Unique

* Lists: incorporate feedback from James

* Lists: incorporate feedback from Guillaume
---
 CHANGELOG.md                                  | 104 +++++++++++++++-
 .../Membership/Propositional/Properties.agda  | 112 ++++++++++++++----
 .../Propositional/Properties/Core.agda        |   8 +-
 .../Propositional/Properties/WithK.agda       |  20 +++-
 .../List/Membership/Setoid/Properties.agda    |  69 +++++++++--
 src/Data/List/Properties.agda                 |   8 ++
 .../Disjoint/Propositional/Properties.agda    |  65 ++++++++++
 .../Binary/Disjoint/Setoid/Properties.agda    |  48 ++++----
 .../Propositional/Properties/WithK.agda       |  54 +++++++++
 .../Sublist/Heterogeneous/Properties.agda     |   6 +-
 .../Binary/Sublist/Setoid/Properties.agda     |   7 +-
 .../Subset/Propositional/Properties.agda      |  33 +++++-
 .../Binary/Subset/Setoid/Properties.agda      |  45 ++++++-
 .../List/Relation/Unary/Any/Properties.agda   |  11 ++
 .../Unique/Propositional/Properties.agda      |  18 ++-
 .../Unary/Unique/Setoid/Properties.agda       |  20 ++++
 16 files changed, 558 insertions(+), 70 deletions(-)
 create mode 100644 src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
 create mode 100644 src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 62f9b4b8e5..a513e4978f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -98,6 +98,11 @@ New modules
   Data.List.Relation.Unary.All.Properties.Core
   ```
 
+* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
+  Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties`
+
+* `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
+
 Additions to existing modules
 -----------------------------
 
@@ -120,14 +125,44 @@ Additions to existing modules
 
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
-  Any-∈-swap :  Any (_∈ ys) xs → Any (_∈ xs) ys
-  All-∉-swap :  All (_∉ ys) xs → All (_∉ xs) ys
+  Any-∈-swap     : Any (_∈ ys) xs → Any (_∈ xs) ys
+  All-∉-swap     : All (_∉ ys) xs → All (_∉ xs) ys
+  ∈-map∘filter⁻  : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
+  ∈-map∘filter⁺  : f Preserves _≈₁_ ⟶ _≈₂_ →
+                   ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
+                   y ∈₂ map f (filter P? xs)
+  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∉[]            : x ∉ []
+  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
+  ```
+
+* In `Data.List.Membership.Propositional.Properties`:
+  ```agda
+  ∈-AllPairs₂    : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
+  ∈-map∘filter⁻  : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x)
+  ∈-map∘filter⁺  : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs)
+  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ++-∈⇔          : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  []∉map∷        : [] ∉ map (x ∷_) xss
+  map∷-decomp∈   : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
+  map∷-decomp    : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs
+  ∈-map∷⁻        : xs ∈ map (x ∷_) xss → x ∈ xs
+  ∉[]            : x ∉ []
+  deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
+  ```
+
+* In `Data.List.Membership.Propositional.Properties.WithK`:
+  ```agda
+  unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
   ```
 
 * In `Data.List.Properties`:
   ```agda
-  product≢0 : All NonZero ns → NonZero (product ns)
-  ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
+  product≢0    : All NonZero ns → NonZero (product ns)
+  ∈⇒≤product   : All NonZero ns → n ∈ ns → n ≤ product ns
+  concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
   ```
 
 * In `Data.List.Relation.Unary.All`:
@@ -135,6 +170,22 @@ Additions to existing modules
   search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
   ```
 
+* In `Data.List.Relation.Unary.Any.Properties`:
+  ```agda
+  concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
+  concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
+  ```
+
+* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
+  ```agda
+  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
+  ```
+
+* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
+  ```agda
+  Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
+  ```
+
 * In `Data.List.Relation.Binary.Equality.Setoid`:
   ```agda
   ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
@@ -147,6 +198,51 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
+  ```agda
+  ∷⊈[]   : x ∷ xs ⊈ []
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ```
+
+* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  ∷⊈[]   : x ∷ xs ⊈ []
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ```
+
+* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
+  ```
+
+* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
+  ```agda
+  Sublist-[]-universal : Universal (Sublist R [])
+  ```
+
+* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
+  ```agda
+  []⊆-universal : Universal ([] ⊆_)
+  ```
+
+* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
+  ```agda
+  deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  ```
+
+* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
+  ```agda
+  deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
+  ```agda
+  dedup-++-↭ : Disjoint xs ys →
+               deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
+  ```
+
 * In `Data.Maybe.Properties`:
   ```agda
   maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 03e31d8aae..39204f19e2 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -24,16 +24,16 @@ open import Data.List.Relation.Unary.Any.Properties
 open import Data.Nat.Base using (ℕ; suc; s≤s; _≤_; _<_; _≰_)
 open import Data.Nat.Properties
   using (suc-injective; m≤n⇒m≤1+n; _≤?_; <⇒≢; ≰⇒>)
-open import Data.Product.Base using (∃; ∃₂; _×_; _,_)
+open import Data.Product.Base using (∃; ∃₂; _×_; _,_; ∃-syntax; -,_; map₂)
 open import Data.Product.Properties using (×-≡,≡↔≡)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Effect.Monad using (RawMonad)
-open import Function.Base using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_)
+open import Function.Base using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_; _∋_)
 open import Function.Definitions using (Injective)
 import Function.Related.Propositional as Related
-open import Function.Bundles using (_↔_; _↣_; Injection)
+open import Function.Bundles using (_↔_; _↣_; Injection; _⇔_; mk⇔)
 open import Function.Related.TypeIsomorphisms using (×-comm; ∃∃↔∃∃)
 open import Function.Construct.Identity using (↔-id)
 open import Level using (Level)
@@ -55,6 +55,9 @@ private
   variable
     ℓ : Level
     A B C : Set ℓ
+    x y v : A
+    xs ys : List A
+    xss : List (List A)
 
 ------------------------------------------------------------------------
 -- Publicly re-export properties from Core
@@ -64,10 +67,10 @@ open import Data.List.Membership.Propositional.Properties.Core public
 ------------------------------------------------------------------------
 -- Equality
 
-∈-resp-≋ : ∀ {x : A} → (x ∈_) Respects _≋_
+∈-resp-≋ : (x ∈_) Respects _≋_
 ∈-resp-≋ = Membership.∈-resp-≋ (≡.setoid _)
 
-∉-resp-≋ : ∀ {x : A} → (x ∉_) Respects _≋_
+∉-resp-≋ : (x ∉_) Respects _≋_
 ∉-resp-≋ = Membership.∉-resp-≋ (≡.setoid _)
 
 ------------------------------------------------------------------------
@@ -96,14 +99,14 @@ map-mapWith∈ = Membership.map-mapWith∈ (≡.setoid _)
 
 module _ (f : A → B) where
 
-  ∈-map⁺ : ∀ {x xs} → x ∈ xs → f x ∈ map f xs
+  ∈-map⁺ : x ∈ xs → f x ∈ map f xs
   ∈-map⁺ = Membership.∈-map⁺ (≡.setoid A) (≡.setoid B) (cong f)
 
-  ∈-map⁻ : ∀ {y xs} → y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x
+  ∈-map⁻ : y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x
   ∈-map⁻ = Membership.∈-map⁻ (≡.setoid A) (≡.setoid B)
 
-  map-∈↔ : ∀ {y xs} → (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs
-  map-∈↔ {y} {xs} =
+  map-∈↔ : (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs
+  map-∈↔ {xs} {y} =
     (∃ λ x → x ∈ xs × y ≡ f x)   ↔⟨ Any↔ ⟩
     Any (λ x → y ≡ f x) xs       ↔⟨ map↔ ⟩
     y ∈ List.map f xs            ∎
@@ -114,7 +117,7 @@ module _ (f : A → B) where
 
 module _ {v : A} where
 
-  ∈-++⁺ˡ : ∀ {xs ys} → v ∈ xs → v ∈ xs ++ ys
+  ∈-++⁺ˡ : v ∈ xs → v ∈ xs ++ ys
   ∈-++⁺ˡ = Membership.∈-++⁺ˡ (≡.setoid A)
 
   ∈-++⁺ʳ : ∀ xs {ys} → v ∈ ys → v ∈ xs ++ ys
@@ -123,10 +126,13 @@ module _ {v : A} where
   ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
   ∈-++⁻ = Membership.∈-++⁻ (≡.setoid A)
 
+  ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  ++-∈⇔ = mk⇔ (∈-++⁻ _) Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ]
+
   ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys
   ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl
 
-  ∈-∃++ : ∀ {xs} → v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs
+  ∈-∃++ : v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs
   ∈-∃++ v∈xs
     with ys , zs , _ , refl , eq ← Membership.∈-∃++ (≡.setoid A) v∈xs
     = ys , zs , ≋⇒≡ eq
@@ -136,7 +142,7 @@ module _ {v : A} where
 
 module _ {v : A} where
 
-  ∈-concat⁺ : ∀ {xss} → Any (v ∈_) xss → v ∈ concat xss
+  ∈-concat⁺ : Any (v ∈_) xss → v ∈ concat xss
   ∈-concat⁺ = Membership.∈-concat⁺ (≡.setoid A)
 
   ∈-concat⁻ : ∀ xss → v ∈ concat xss → Any (v ∈_) xss
@@ -151,8 +157,7 @@ module _ {v : A} where
     let xs , v∈xs , xs∈xss = Membership.∈-concat⁻′ (≡.setoid A) xss v∈c
     in xs , v∈xs , Any.map ≋⇒≡ xs∈xss
 
-  concat-∈↔ : ∀ {xss : List (List A)} →
-              (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss
+  concat-∈↔ : (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss
   concat-∈↔ {xss} =
     (∃ λ xs → v ∈ xs × xs ∈ xss)  ↔⟨ Σ.cong (↔-id _) $ ×-comm _ _ ⟩
     (∃ λ xs → xs ∈ xss × v ∈ xs)  ↔⟨ Any↔ ⟩
@@ -160,6 +165,19 @@ module _ {v : A} where
     v ∈ concat xss                ∎
     where open Related.EquationalReasoning
 
+------------------------------------------------------------------------
+-- concatMap
+
+module _ (f : A → List B) {xs y} where
+
+  private Sᴬ = ≡.setoid A; Sᴮ = ≡.setoid B
+
+  ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁺ = Membership.∈-concatMap⁺ Sᴬ Sᴮ
+
+  ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∈-concatMap⁻ = Membership.∈-concatMap⁻ Sᴬ Sᴮ
+
 ------------------------------------------------------------------------
 -- cartesianProductWith
 
@@ -246,12 +264,25 @@ module _ {n} {f : Fin n → A} where
 
 module _ {p} {P : A → Set p} (P? : Decidable P) where
 
-  ∈-filter⁺ : ∀ {x xs} → x ∈ xs → P x → x ∈ filter P? xs
+  ∈-filter⁺ : x ∈ xs → P x → x ∈ filter P? xs
   ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (≡.resp P)
 
-  ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
+  ∈-filter⁻ : v ∈ filter P? xs → v ∈ xs × P v
   ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (≡.resp P)
 
+------------------------------------------------------------------------
+-- map∘filter
+
+module _ (f : A → B) {p} {P : A → Set p} (P? : Decidable P) {f xs y} where
+
+  private Sᴬ = ≡.setoid A; Sᴮ = ≡.setoid B; respP = ≡.resp P
+
+  ∈-map∘filter⁻ : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x)
+  ∈-map∘filter⁻ = Membership.∈-map∘filter⁻ Sᴬ Sᴮ P? respP
+
+  ∈-map∘filter⁺ : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs)
+  ∈-map∘filter⁺ = Membership.∈-map∘filter⁺ Sᴬ Sᴮ P? respP (cong f)
+
 ------------------------------------------------------------------------
 -- derun and deduplicate
 
@@ -268,8 +299,13 @@ module _ (_≈?_ : DecidableEquality A) where
   ∈-derun⁺ : ∀ {xs z} → z ∈ xs → z ∈ derun _≈?_ xs
   ∈-derun⁺ z∈xs = Membership.∈-derun⁺ (≡.setoid A) _≈?_ (flip trans) z∈xs
 
+  private resp≈ = λ {c b a : A} (c≡b : c ≡ b) (a≡b : a ≡ b) → trans a≡b (sym c≡b)
+
   ∈-deduplicate⁺ : ∀ {xs z} → z ∈ xs → z ∈ deduplicate _≈?_ xs
-  ∈-deduplicate⁺ z∈xs = Membership.∈-deduplicate⁺ (≡.setoid A) _≈?_ (λ c≡b a≡b → trans a≡b (sym c≡b)) z∈xs
+  ∈-deduplicate⁺ z∈xs = Membership.∈-deduplicate⁺ (≡.setoid A) _≈?_ resp≈ z∈xs
+
+  deduplicate-∈⇔ : ∀ {xs z} → z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
+  deduplicate-∈⇔ = Membership.deduplicate-∈⇔ (≡.setoid A) _≈?_ resp≈
 
 ------------------------------------------------------------------------
 -- _>>=_
@@ -310,13 +346,13 @@ module _ (_≈?_ : DecidableEquality A) where
 ------------------------------------------------------------------------
 -- length
 
-∈-length : ∀ {x : A} {xs} → x ∈ xs → 0 < length xs
+∈-length : x ∈ xs → 0 < length xs
 ∈-length = Membership.∈-length (≡.setoid _)
 
 ------------------------------------------------------------------------
 -- lookup
 
-∈-lookup : ∀ {xs : List A} i → lookup xs i ∈ xs
+∈-lookup : ∀ i → lookup xs i ∈ xs
 ∈-lookup {xs = xs} i = Membership.∈-lookup (≡.setoid _) xs i
 
 ------------------------------------------------------------------------
@@ -337,7 +373,7 @@ module _ {_•_ : Op₂ A} where
 ------------------------------------------------------------------------
 -- inits
 
-[]∈inits : ∀ {a} {A : Set a} (as : List A) → [] ∈ inits as
+[]∈inits : (as : List A) → [] ∈ inits as
 []∈inits _ = here refl
 
 ------------------------------------------------------------------------
@@ -401,3 +437,39 @@ there-injective-≢∈ : ∀ {xs} {x y z : A} {x∈xs : x ∈ xs} {y∈xs : y 
                      there {x = z} x∈xs ≢∈ there y∈xs →
                      x∈xs ≢∈ y∈xs
 there-injective-≢∈ neq refl eq = neq refl (≡.cong there eq)
+
+------------------------------------------------------------------------
+-- AllPairs
+
+open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
+import Data.List.Relation.Unary.All as All
+
+module _ {R : A → A → Set ℓ} where
+  ∈-AllPairs₂ : ∀ {xs x y} → AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
+  ∈-AllPairs₂ (_ ∷ _)  (here refl) (here refl) = inj₁ refl
+  ∈-AllPairs₂ (p ∷ _)  (here refl) (there y∈)  = inj₂ $ inj₁ $ All.lookup p y∈
+  ∈-AllPairs₂ (p ∷ _)  (there x∈)  (here refl) = inj₂ $ inj₂ $ All.lookup p x∈
+  ∈-AllPairs₂ (_ ∷ ps) (there x∈)  (there y∈)  = ∈-AllPairs₂ ps x∈ y∈
+
+------------------------------------------------------------------------
+-- nested lists
+
+[]∉map∷ : (List A ∋ []) ∉ map (x ∷_) xss
+[]∉map∷ {xss = _ ∷ _} (there p) = []∉map∷ p
+
+map∷-decomp∈ : (List A ∋ x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
+map∷-decomp∈ {xss = _ ∷ _} = λ where
+  (here refl) → refl , here refl
+  (there p)   → map₂ there $ map∷-decomp∈ p
+
+map∷-decomp : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs
+map∷-decomp               {xss = _  ∷ _} (here refl) = -, here refl , refl
+map∷-decomp {xs = []}     {xss = _  ∷ _} (there xs∈) = contradiction xs∈ []∉map∷
+map∷-decomp {xs = x ∷ xs} {xss = _  ∷ _} (there xs∈) =
+  let eq , p = map∷-decomp∈ xs∈
+  in -, there p , cong (_∷ _) (sym eq)
+
+∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs
+∈-map∷⁻ {xss = _ ∷ _} = λ where
+  (here refl) → here refl
+  (there p)   → ∈-map∷⁻ p
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index 5c77e40b96..65485abb0e 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -12,7 +12,7 @@
 
 module Data.List.Membership.Propositional.Properties.Core where
 
-open import Data.List.Base using (List)
+open import Data.List.Base using (List; [])
 open import Data.List.Membership.Propositional
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product.Base as Product using (_,_; ∃; _×_)
@@ -30,6 +30,12 @@ private
     x : A
     xs : List A
 
+------------------------------------------------------------------------
+-- Basics
+
+∉[] : x ∉ []
+∉[] ()
+
 ------------------------------------------------------------------------
 -- find satisfies a simple equality when the predicate is a
 -- propositional equality.
diff --git a/src/Data/List/Membership/Propositional/Properties/WithK.agda b/src/Data/List/Membership/Propositional/Properties/WithK.agda
index a86f23a8ea..656ec11dae 100644
--- a/src/Data/List/Membership/Propositional/Properties/WithK.agda
+++ b/src/Data/List/Membership/Propositional/Properties/WithK.agda
@@ -9,17 +9,31 @@
 
 module Data.List.Membership.Propositional.Properties.WithK where
 
+open import Level using (Level)
+open import Function.Bundles using (Equivalence)
 open import Data.List.Base
 open import Data.List.Relation.Unary.Unique.Propositional
 open import Data.List.Membership.Propositional
 import Data.List.Membership.Setoid.Properties as Membership
+open import Data.List.Relation.Binary.BagAndSetEquality using (_∼[_]_; set; bag)
+open import Data.Product using (_,_)
 open import Relation.Unary using (Irrelevant)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Relation.Binary.PropositionalEquality.WithK
+open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)
+
+private
+  variable
+    a : Level
+    A : Set a
+    xs ys : List A
 
 ------------------------------------------------------------------------
 -- Irrelevance
 
-unique⇒irrelevant : ∀ {a} {A : Set a} {xs : List A} →
-                    Unique xs → Irrelevant (_∈ xs)
+unique⇒irrelevant : Unique xs → Irrelevant (_∈ xs)
 unique⇒irrelevant = Membership.unique⇒irrelevant (≡.setoid _) ≡-irrelevant
+
+unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
+unique∧set⇒bag p p′ eq = record
+  { Equivalence eq
+  ; inverse = (λ _ → unique⇒irrelevant p′ _ _) , (λ _ → unique⇒irrelevant p _ _) }
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 76bbd8beaf..c17fa15b98 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -1,4 +1,4 @@
-------------------------------------------------------------------------
+-----------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to setoid list membership
@@ -21,11 +21,11 @@ import Data.List.Relation.Unary.All.Properties.Core as All
 import Data.List.Relation.Unary.Any.Properties as Any
 import Data.List.Relation.Unary.Unique.Setoid as Unique
 open import Data.Nat.Base using (suc; z<s; _<_)
-open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂)
+open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂; ∃-syntax)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_$_; flip; _∘_; _∘′_; id)
-open import Function.Bundles using (_↔_)
+open import Function.Bundles using (_↔_; mk↔; _⇔_; mk⇔)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_; _Preserves_⟶_)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
@@ -42,6 +42,16 @@ private
   variable
     c c₁ c₂ c₃ p ℓ ℓ₁ ℓ₂ ℓ₃ : Level
 
+------------------------------------------------------------------------
+-- Basics
+
+module _ (S : Setoid c ℓ) where
+
+  open Membership S
+
+  ∉[] : ∀ {x} → x ∉ []
+  ∉[] ()
+
 ------------------------------------------------------------------------
 -- Equality properties
 
@@ -239,6 +249,21 @@ module _ (S : Setoid c ℓ) where
   ∈-concat⁻′ xss v∈c[xss] =
     let xs , xs∈xss , v∈xs = find (∈-concat⁻ xss v∈c[xss]) in xs , v∈xs , xs∈xss
 
+------------------------------------------------------------------------
+-- concatMap
+
+module _
+  (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂)
+  {f : Carrier S₁ → List (Carrier S₂)} {xs y} where
+
+  open Membership S₂ using (_∈_)
+
+  ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁺ = Any.concatMap⁺ f
+
+  ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∈-concatMap⁻ = Any.concatMap⁻ f
+
 ------------------------------------------------------------------------
 -- reverse
 
@@ -363,6 +388,33 @@ module _ (S : Setoid c ℓ) {P : Pred (Carrier S) p}
   ...   | here  v≈x   = here v≈x , resp (sym v≈x) (invert [Px])
   ...   | there v∈fxs = Product.map there id (∈-filter⁻ v∈fxs)
 
+------------------------------------------------------------------------
+-- map∘filter
+
+module _
+  (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂)
+  {P : Pred _ p} (P? : Decidable P) (resp : P Respects _)
+  {f xs y} where
+
+  open Setoid     S₁ renaming (_≈_ to _≈₁_)
+  open Setoid     S₂ renaming (_≈_ to _≈₂_; sym to sym₂)
+  open Membership S₁ renaming (_∈_ to _∈₁_)
+  open Membership S₂ renaming (_∈_ to _∈₂_)
+
+  ∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) →
+                  ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
+  ∈-map∘filter⁻ h =
+    let x , x∈ , y≈ = ∈-map⁻ S₁ S₂ h
+        y∈ , Py     = ∈-filter⁻ S₁ P? resp x∈
+    in x , y∈ , y≈ , Py
+
+  ∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ →
+                  ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
+                  y ∈₂ map f (filter P? xs)
+  ∈-map∘filter⁺ pres (x , x∈ , y≈ , Px)
+    = ∈-resp-≈ S₂ (sym₂ y≈)
+    $ ∈-map⁺ S₁ S₂ pres (∈-filter⁺ S₁ P? resp x∈ Px)
+
 ------------------------------------------------------------------------
 -- derun and deduplicate
 
@@ -374,16 +426,20 @@ module _ (S : Setoid c ℓ) {R : Rel (Carrier S) ℓ₂} (R? : Binary.Decidable
   ∈-derun⁺ : _≈_ Respectsʳ R → ∀ {xs z} → z ∈ xs → z ∈ derun R? xs
   ∈-derun⁺ ≈-resp-R z∈xs = Any.derun⁺ R? ≈-resp-R z∈xs
 
+  ∈-derun⁻ : ∀ xs {z} → z ∈ derun R? xs → z ∈ xs
+  ∈-derun⁻ xs z∈derun[R,xs] = Any.derun⁻ R? z∈derun[R,xs]
+
   ∈-deduplicate⁺ : _≈_ Respectsʳ (flip R) → ∀ {xs z} →
                    z ∈ xs → z ∈ deduplicate R? xs
   ∈-deduplicate⁺ ≈-resp-R z∈xs = Any.deduplicate⁺ R? ≈-resp-R z∈xs
 
-  ∈-derun⁻ : ∀ xs {z} → z ∈ derun R? xs → z ∈ xs
-  ∈-derun⁻ xs z∈derun[R,xs] = Any.derun⁻ R? z∈derun[R,xs]
-
   ∈-deduplicate⁻ : ∀ xs {z} → z ∈ deduplicate R? xs → z ∈ xs
   ∈-deduplicate⁻ xs z∈dedup[R,xs] = Any.deduplicate⁻ R? z∈dedup[R,xs]
 
+  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → ∀ {xs z} →
+                   z ∈ xs ⇔ z ∈ deduplicate R? xs
+  deduplicate-∈⇔ p = mk⇔ (∈-deduplicate⁺ p) (∈-deduplicate⁻ _)
+
 ------------------------------------------------------------------------
 -- length
 
@@ -461,4 +517,3 @@ module _ (S : Setoid c ℓ) where
 
   All-∉-swap :  ∀ {xs ys} → All (_∉ ys) xs → All (_∉ xs) ys
   All-∉-swap p = All.¬Any⇒All¬ _ ((All.All¬⇒¬Any p) ∘ Any-∈-swap)
-
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index f847d8a059..71d7b90b7f 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -715,6 +715,14 @@ map-concatMap f g xs = begin
   concatMap (map f ∘′ g) xs
     ∎
 
+concatMap-++ : ∀ (f : A → List B) xs ys →
+               concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
+concatMap-++ f xs ys = begin
+  concatMap f (xs ++ ys)           ≡⟨⟩
+  concat (map f (xs ++ ys))        ≡⟨ cong concat $ map-++ f xs ys ⟩
+  concat (map f xs ++ map f ys)    ≡˘⟨ concat-++ (map f xs) (map f ys) ⟩
+  concatMap f xs ++ concatMap f ys ∎ where open ≡-Reasoning
+
 ------------------------------------------------------------------------
 -- catMaybes
 
diff --git a/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
new file mode 100644
index 0000000000..b2b2ec591c
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
@@ -0,0 +1,65 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of disjoint lists (propositional equality)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Binary.Disjoint.Propositional.Properties where
+
+open import Level using (Level)
+open import Function.Base using (_∘_)
+open import Function.Bundles using (_⇔_)
+open import Data.List.Base
+open import Data.List.Relation.Binary.Disjoint.Propositional
+import Data.List.Relation.Unary.Any as Any
+open import Data.List.Relation.Unary.All as All
+open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
+open import Data.List.Relation.Unary.Any.Properties using (++⁻)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.Product.Base as Product using (_,_)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Symmetric; DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Relation.Nullary.Negation using (¬_)
+
+import Data.List.Relation.Binary.Disjoint.Setoid.Properties as S
+
+module _ {a} {A : Set a} where
+
+  private
+    Sᴬ = setoid A
+    variable
+      x : A
+      xs ys vs : List A
+      xss : List (List A)
+
+  ------------------------------------------------------------------------
+  -- Relational properties
+  ------------------------------------------------------------------------
+
+  sym : Symmetric Disjoint
+  sym = S.sym Sᴬ
+
+  ------------------------------------------------------------------------
+  -- Relationship with other predicates
+  ------------------------------------------------------------------------
+
+  Disjoint⇒AllAll : Disjoint xs ys → All (λ x → All (λ y → ¬ x ≡ y) ys) xs
+  Disjoint⇒AllAll = S.Disjoint⇒AllAll Sᴬ
+
+  ------------------------------------------------------------------------
+  -- Introduction (⁺) and elimination (⁻) rules for list operations
+  ------------------------------------------------------------------------
+  -- concat
+
+  concat⁺ʳ : All (Disjoint vs) xss → Disjoint vs (concat xss)
+  concat⁺ʳ = S.concat⁺ʳ (setoid _)
+
+  -- deduplicate
+  module _ (_≟_ : DecidableEquality A) where
+    deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+    deduplicate⁺ = S.deduplicate⁺ Sᴬ _≟_
diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
index bc5a95fc77..3416fc31e8 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
@@ -8,49 +8,57 @@
 
 module Data.List.Relation.Binary.Disjoint.Setoid.Properties where
 
+open import Function.Base using (_∘_)
+open import Function.Bundles using (_⇔_; mk⇔)
 open import Data.List.Base
 open import Data.List.Relation.Binary.Disjoint.Setoid
 import Data.List.Relation.Unary.Any as Any
 open import Data.List.Relation.Unary.All as All
 open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
 open import Data.List.Relation.Unary.Any.Properties using (++⁻)
-open import Data.Product.Base using (_,_)
+import Data.List.Membership.Setoid.Properties as Mem
+open import Data.Product.Base as Product using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions using (Symmetric)
+open import Relation.Binary.Definitions using (Symmetric; DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Nullary.Negation using (¬_)
 
-------------------------------------------------------------------------
--- Relational properties
-------------------------------------------------------------------------
-
 module _ {c ℓ} (S : Setoid c ℓ) where
 
-  sym : Symmetric (Disjoint S)
-  sym xs#ys (v∈ys , v∈xs) = xs#ys (v∈xs , v∈ys)
+  open Setoid S using (_≉_; reflexive) renaming (Carrier to A)
 
-------------------------------------------------------------------------
--- Relationship with other predicates
-------------------------------------------------------------------------
+  ------------------------------------------------------------------------
+  -- Relational properties
+  ------------------------------------------------------------------------
 
-module _ {c ℓ} (S : Setoid c ℓ) where
+  sym : Symmetric (Disjoint S)
+  sym xs#ys (v∈ys , v∈xs) = xs#ys (v∈xs , v∈ys)
 
-  open Setoid S
+  ------------------------------------------------------------------------
+  -- Relationship with other predicates
+  ------------------------------------------------------------------------
 
   Disjoint⇒AllAll : ∀ {xs ys} → Disjoint S xs ys →
-                    All (λ x → All (λ y → ¬ x ≈ y) ys) xs
+                    All (λ x → All (x ≉_) ys) xs
   Disjoint⇒AllAll xs#ys = All.map (¬Any⇒All¬ _)
     (All.tabulate (λ v∈xs v∈ys → xs#ys (Any.map reflexive v∈xs , v∈ys)))
 
-------------------------------------------------------------------------
--- Introduction (⁺) and elimination (⁻) rules for list operations
-------------------------------------------------------------------------
--- concat
-
-module _ {c ℓ} (S : Setoid c ℓ) where
+  ------------------------------------------------------------------------
+  -- Introduction (⁺) and elimination (⁻) rules for list operations
+  ------------------------------------------------------------------------
+  -- concat
 
   concat⁺ʳ : ∀ {vs xss} → All (Disjoint S vs) xss → Disjoint S vs (concat xss)
   concat⁺ʳ {xss = xs ∷ xss} (vs#xs ∷ vs#xss) (v∈vs , v∈xs++concatxss)
     with ++⁻ xs v∈xs++concatxss
   ... | inj₁ v∈xs  = vs#xs (v∈vs , v∈xs)
   ... | inj₂ v∈xss = concat⁺ʳ vs#xss (v∈vs , v∈xss)
+
+  -- deduplicate
+  module _ (_≟_ : DecidableEquality A) where
+
+    deduplicate⁺ : ∀ {xs ys} → Disjoint S xs ys →
+                   Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+    deduplicate⁺ = let ∈-dedup⁻ = Mem.∈-deduplicate⁻ S _≟_ in
+      _∘ Product.map (∈-dedup⁻ _) (∈-dedup⁻ _)
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
new file mode 100644
index 0000000000..3bed7656fc
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
@@ -0,0 +1,54 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of permutation (with K)
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --with-K #-}
+
+module Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK where
+
+open import Function.Base using (_$_)
+open import Function.Bundles using (_⇔_; mk⇔)
+open import Function.Related.Propositional using (SK-sym; module EquationalReasoning)
+
+open import Data.List.Base using (deduplicate; _++_)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties using (++-∈⇔; deduplicate-∈⇔)
+open import Data.List.Membership.Propositional.Properties.WithK using (unique∧set⇒bag)
+open import Data.List.Relation.Unary.Unique.Propositional.Properties using (++⁺)
+open import Data.List.Relation.Binary.Disjoint.Propositional using (Disjoint)
+open import Data.List.Relation.Binary.Disjoint.Propositional.Properties
+  using (deduplicate⁺)
+open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
+open import Data.List.Relation.Binary.BagAndSetEquality using (∼bag⇒↭)
+
+open import Data.Sum as Sum using (_⊎_)
+open import Data.Sum.Function.Propositional using (_⊎-cong_)
+
+open import Relation.Binary.Definitions using (DecidableEquality)
+
+------------------------------------------------------------------------
+-- deduplicate
+
+module _ {a} {A : Set a} (_≟_ : DecidableEquality A) where
+
+  private
+    dedup≡   = deduplicate    _≟_
+    ∈-dedup≡ = deduplicate-∈⇔ _≟_
+
+  open import Data.List.Relation.Unary.Unique.DecPropositional.Properties _≟_
+    using (deduplicate-!)
+
+  dedup-++-↭ : ∀ {xs ys} → Disjoint xs ys → dedup≡ (xs ++ ys) ↭ dedup≡ xs ++ dedup≡ ys
+  dedup-++-↭ {xs} {ys} disj
+    = ∼bag⇒↭
+    $ unique∧set⇒bag
+        (deduplicate-! _)
+        (++⁺ (deduplicate-! _) (deduplicate-! _) (deduplicate⁺ _≟_ disj))
+    λ {x} → begin
+    x ∈ dedup≡ (xs ++ ys)           ∼⟨ SK-sym ∈-dedup≡ ⟩
+    x ∈ xs ++ ys                    ∼⟨ ++-∈⇔ ⟩
+    (x ∈ xs ⊎ x ∈ ys)               ∼⟨ ∈-dedup≡ ⊎-cong ∈-dedup≡ ⟩
+    (x ∈ dedup≡ xs ⊎ x ∈ dedup≡ ys) ∼⟨ SK-sym ++-∈⇔ ⟩
+    x ∈ dedup≡ xs ++ dedup≡ ys      ∎ where open EquationalReasoning
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
index 8dd94d8b3b..77c2ef5738 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
@@ -331,10 +331,14 @@ module _ {R : REL A B r} where
   ∷ʳ⁻¹ ¬r = mk⇔ (_ ∷ʳ_) (∷ʳ⁻ ¬r)
 
 ------------------------------------------------------------------------
--- Irrelevant special case
+-- Empty special case
 
 module _ {R : REL A B r} where
 
+  Sublist-[]-universal : U.Universal (Sublist R [])
+  Sublist-[]-universal []      = []
+  Sublist-[]-universal (_ ∷ _) = _ ∷ʳ Sublist-[]-universal _
+
   Sublist-[]-irrelevant : U.Irrelevant (Sublist R [])
   Sublist-[]-irrelevant []       []        = ≡.refl
   Sublist-[]-irrelevant (y ∷ʳ p) (.y ∷ʳ q) = ≡.cong (y ∷ʳ_) (Sublist-[]-irrelevant p q)
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index 60be70aac1..b42e33365d 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -24,7 +24,7 @@ open import Level
 open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; cong; cong₂)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
-open import Relation.Unary using (Pred; Decidable; Irrelevant)
+open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable using (¬?; yes; no)
 
@@ -293,7 +293,10 @@ module _ where
   to-≋ = HeteroProperties.toPointwise
 
 ------------------------------------------------------------------------
--- Irrelevant special case
+-- Empty special case
+
+  []⊆-universal : Universal ([] ⊆_)
+  []⊆-universal = HeteroProperties.Sublist-[]-universal
 
   []⊆-irrelevant : Irrelevant ([] ⊆_)
   []⊆-irrelevant = HeteroProperties.Sublist-[]-irrelevant
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
index 75e1a5b00a..4054afc092 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -10,25 +10,25 @@ module Data.List.Relation.Binary.Subset.Propositional.Properties
   where
 
 open import Data.Bool.Base using (Bool; true; false; T)
-open import Data.List.Base using (List; map; _∷_; _++_; concat; applyUpTo;
-  any; filter)
+open import Data.List.Base
+  using (List; []; map; _∷_; _++_; concat; concatMap; applyUpTo; any; filter)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All)
 import Data.List.Relation.Unary.Any.Properties as Any hiding (filter⁺)
 open import Data.List.Effectful using (monad)
 open import Data.List.Relation.Unary.Any using (Any)
-open import Data.List.Membership.Propositional using (_∈_; mapWith∈)
+open import Data.List.Membership.Propositional using (_∈_; _∉_; mapWith∈)
 open import Data.List.Membership.Propositional.Properties
   using (map-∈↔; concat-∈↔; >>=-∈↔; ⊛-∈↔; ⊗-∈↔)
 import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset
 open import Data.List.Relation.Binary.Subset.Propositional
-  using (_⊆_; _⊇_)
+  using (_⊆_; _⊇_; _⊈_)
 open import Data.List.Relation.Binary.Permutation.Propositional
   using (_↭_; ↭-sym; ↭-isEquivalence)
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation
 open import Data.Nat.Base using (ℕ; _≤_)
 import Data.Product.Base as Product
-import Data.Sum.Base as Sum
+open import Data.Sum.Base as Sum using (_⊎_)
 open import Effect.Monad
 open import Function.Base using (_∘_; _∘′_; id; _$_)
 open import Function.Bundles using (_↔_; Inverse; Equivalence)
@@ -52,8 +52,19 @@ private
     a b p q : Level
     A : Set a
     B : Set b
+    x y : A
     ws xs ys zs : List A
 
+------------------------------------------------------------------------
+-- Basics
+------------------------------------------------------------------------
+
+∷⊈[] : x ∷ xs ⊈ []
+∷⊈[] = Subset.∷⊈[] (setoid _)
+
+⊆[]⇒≡[] : ∀ {A : Set a} → (_⊆ []) ⋐ (_≡ [])
+⊆[]⇒≡[] {A = A} = Subset.⊆[]⇒≡[] (setoid A)
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -150,6 +161,12 @@ xs⊆x∷xs = Subset.xs⊆x∷xs (setoid _)
 ∈-∷⁺ʳ : ∀ {x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
 ∈-∷⁺ʳ = Subset.∈-∷⁺ʳ (setoid _)
 
+⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+⊆∷⇒∈∨⊆ = Subset.⊆∷⇒∈∨⊆ (setoid _)
+
+⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+⊆∷∧∉⇒⊆ = Subset.⊆∷∧∉⇒⊆ (setoid _)
+
 ------------------------------------------------------------------------
 -- _++_
 
@@ -179,6 +196,12 @@ module _ {xss yss : List (List A)} where
     Product.map₂ (Product.map₂ xss⊆yss) ∘
     Inverse.from concat-∈↔
 
+------------------------------------------------------------------------
+-- concatMap
+
+concatMap⁺ : ∀ (f : A → List B) → xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
+concatMap⁺ _ = concat⁺ ∘ map⁺ _
+
 ------------------------------------------------------------------------
 -- applyUpTo
 
diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index 0d0d685a27..901ee8b942 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
@@ -22,7 +22,8 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Binary.Permutation.Setoid as Permutation
 import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutationₚ
 open import Data.Product.Base using (_,_)
-open import Function.Base using (_∘_; _∘₂_; _$_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Function.Base using (_∘_; _∘₂_; _$_; case_of_)
 open import Level using (Level)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
@@ -34,6 +35,7 @@ open import Relation.Binary.Bundles using (Setoid; Preorder)
 open import Relation.Binary.Structures using (IsPreorder)
 import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
 open import Relation.Binary.Reasoning.Syntax
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 open Setoid using (Carrier)
 
@@ -41,6 +43,22 @@ private
   variable
     a b p q r ℓ : Level
 
+------------------------------------------------------------------------
+-- Basics
+------------------------------------------------------------------------
+
+module _ (S : Setoid a ℓ) where
+
+  open Setoid S using (refl)
+  open Subset S
+
+  ∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
+  ∷⊈[] p = Membershipₚ.∉[] S $ p (here refl)
+
+  ⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ [])
+  ⊆[]⇒≡[] {x = []}    _ = ≡.refl
+  ⊆[]⇒≡[] {x = _ ∷ _} p with () ← ∷⊈[] p
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -161,12 +179,14 @@ module _ (S : Setoid a ℓ) where
 
 ------------------------------------------------------------------------
 -- Properties of list functions
+------------------------------------------------------------------------
+
 ------------------------------------------------------------------------
 -- ∷
 
 module _ (S : Setoid a ℓ) where
 
-  open Setoid S
+  open Setoid S renaming (Carrier to A)
   open Subset S
   open Membership S
   open Membershipₚ
@@ -174,14 +194,31 @@ module _ (S : Setoid a ℓ) where
   xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs
   xs⊆x∷xs xs x = there
 
-  ∷⁺ʳ : ∀ {xs ys} x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
+  private variable
+    x y : A
+    xs ys : List A
+
+  ∷⁺ʳ : ∀ x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
   ∷⁺ʳ x xs⊆ys (here  p) = here p
   ∷⁺ʳ x xs⊆ys (there p) = there (xs⊆ys p)
 
-  ∈-∷⁺ʳ : ∀ {xs ys x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
+  ∈-∷⁺ʳ : x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
   ∈-∷⁺ʳ x∈ys _  (here  v≈x)  = ∈-resp-≈ S (sym v≈x) x∈ys
   ∈-∷⁺ʳ _ xs⊆ys (there x∈xs) = xs⊆ys x∈xs
 
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷⇒∈∨⊆ {xs = []}       []⊆y∷ys = inj₂ λ ()
+  ⊆∷⇒∈∨⊆ {xs = _ ∷ _} x∷xs⊆y∷ys with ⊆∷⇒∈∨⊆ $ x∷xs⊆y∷ys ∘ there
+  ... | inj₁ y∈xs  = inj₁ $ there y∈xs
+  ... | inj₂ xs⊆ys with x∷xs⊆y∷ys (here refl)
+  ...   | here x≈y = inj₁ $ here (sym x≈y)
+  ...   | there x∈ys = inj₂ (∈-∷⁺ʳ x∈ys xs⊆ys)
+
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ⊆∷∧∉⇒⊆ xs⊆y∷ys y∉xs with ⊆∷⇒∈∨⊆ xs⊆y∷ys
+  ... | inj₁ y∈xs  = contradiction y∈xs y∉xs
+  ... | inj₂ xs⊆ys = xs⊆ys
+
 ------------------------------------------------------------------------
 -- ++
 
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 836e73d4a4..6f1df8cbcc 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -461,6 +461,17 @@ module _ {P : A → Set p} where
   concat↔ : ∀ {xss} → Any (Any P) xss ↔ Any P (concat xss)
   concat↔ {xss} = mk↔ₛ′ concat⁺ (concat⁻ xss) (concat⁺∘concat⁻ xss) concat⁻∘concat⁺
 
+------------------------------------------------------------------------
+-- concatMap
+
+module _ (f : A → List B) {p} {P : Pred B p} where
+
+  concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
+  concatMap⁺ = concat⁺ ∘ map⁺
+
+  concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
+  concatMap⁻ = map⁻ ∘ concat⁻ _
+
 ------------------------------------------------------------------------
 -- cartesianProductWith
 
diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
index bcd7df1176..8852bdd704 100644
--- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
@@ -8,9 +8,12 @@
 
 module Data.List.Relation.Unary.Unique.Propositional.Properties where
 
-open import Data.List.Base using (map; _++_; concat; cartesianProductWith;
-  cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom;
-  tabulate; allFin; filter)
+open import Data.List.Base
+  using ( List; _∷_; map; _++_; concat; cartesianProductWith
+        ; cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom
+        ; tabulate; allFin; filter
+        )
+open import Data.List.Membership.Propositional using (_∉_)
 open import Data.List.Relation.Binary.Disjoint.Propositional
   using (Disjoint)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
@@ -35,6 +38,9 @@ open import Relation.Nullary.Negation using (¬_)
 private
   variable
     a b c p : Level
+    A : Set a
+    x y : A
+    xs : List A
 
 ------------------------------------------------------------------------
 -- Introduction (⁺) and elimination (⁻) rules for list operations
@@ -154,3 +160,9 @@ module _ {A : Set a} {P : Pred _ p} (P? : Decidable P) where
 
   filter⁺ : ∀ {xs} → Unique xs → Unique (filter P? xs)
   filter⁺ = Setoid.filter⁺ (setoid A) P?
+
+------------------------------------------------------------------------
+-- ∷
+
+Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
+Unique[x∷xs]⇒x∉xs = Setoid.Unique[x∷xs]⇒x∉xs (setoid _)
diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
index ffb587018a..0dc7027c79 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
@@ -9,9 +9,11 @@
 module Data.List.Relation.Unary.Unique.Setoid.Properties where
 
 open import Data.List.Base
+import Data.List.Membership.Setoid as Membership
 open import Data.List.Membership.Setoid.Properties
 open import Data.List.Relation.Binary.Disjoint.Setoid
 open import Data.List.Relation.Binary.Disjoint.Setoid.Properties
+open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any)
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
@@ -156,3 +158,21 @@ module _ (S : Setoid a ℓ) {P : Pred _ p} (P? : Decidable P) where
 
   filter⁺ : ∀ {xs} → Unique S xs → Unique S (filter P? xs)
   filter⁺ = AllPairs.filter⁺ P?
+
+------------------------------------------------------------------------
+-- ∷
+
+module _ (S : Setoid a ℓ) where
+
+  open Setoid S renaming (Carrier to A)
+  open Membership S using (_∉_)
+
+  private
+    variable
+      x y : A
+      xs : List A
+
+  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
+  Unique[x∷xs]⇒x∉xs ((x≉ ∷ x∉) ∷ _ ∷ uniq) = λ where
+    (here x≈)  → x≉ x≈
+    (there x∈) → Unique[x∷xs]⇒x∉xs (x∉ AllPairs.∷ uniq) x∈