From 51731360050d507cca3a7e4ed9ea7f01271abb9f Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Fri, 5 Jul 2024 14:31:31 +0100
Subject: [PATCH 01/13] Lists: irrelevance of membership (in unique lists)

---
 CHANGELOG.md                                  |  5 +++++
 .../Propositional/Properties/WithK.agda       | 20 ++++++++++++++++---
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 62f9b4b8e5..55697a48d6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -124,6 +124,11 @@ Additions to existing modules
   All-∉-swap :  All (_∉ ys) xs → All (_∉ xs) ys
   ```
 
+* 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)
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 _ _) }

From 0324cda1d599a561ddc079d07148144c89b7100e Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Fri, 5 Jul 2024 14:32:09 +0100
Subject: [PATCH 02/13] Lists: the empty list is always a sublist of another

---
 CHANGELOG.md                                           | 10 ++++++++++
 .../Binary/Sublist/Heterogeneous/Properties.agda       |  6 +++++-
 .../Relation/Binary/Sublist/Setoid/Properties.agda     |  7 +++++--
 3 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 55697a48d6..162a8c032a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -152,6 +152,16 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* 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.Maybe.Properties`:
   ```agda
   maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
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

From 651aedacbd00622afa4ea65b6163411122fc2c16 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Fri, 5 Jul 2024 14:58:28 +0100
Subject: [PATCH 03/13] Lists: lookupMaybe (unsafe version of lookup)

---
 CHANGELOG.md            | 5 +++++
 src/Data/List/Base.agda | 6 ++++++
 2 files changed, 11 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 162a8c032a..7c43ffc092 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -118,6 +118,11 @@ Additions to existing modules
   Env = Vec Carrier
  ```
 
+* In `Data.List.Base`:
+  ```agda
+  lookupMaybe : List A → ℕ → Maybe A
+  ```
+
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
   Any-∈-swap :  Any (_∈ ys) xs → Any (_∈ xs) ys
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 0c63e34940..3bc51ec307 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -229,6 +229,12 @@ lookup : ∀ (xs : List A) → Fin (length xs) → A
 lookup (x ∷ xs) zero    = x
 lookup (x ∷ xs) (suc i) = lookup xs i
 
+lookupMaybe : List A → ℕ → Maybe A
+lookupMaybe = λ where
+  []       _       → nothing
+  (x ∷ _)  zero    → just x
+  (_ ∷ xs) (suc n) → lookupMaybe xs n
+
 -- Numerical
 
 upTo : ℕ → List ℕ

From 2fbf5045ddd5796241a13bceedff5d89346e6956 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Fri, 5 Jul 2024 18:09:10 +0100
Subject: [PATCH 04/13] =?UTF-8?q?List:=20`concatMap=E2=81=BA`=20for=20the?=
 =?UTF-8?q?=20subset=20relation?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                                           |  5 +++++
 .../Binary/Subset/Propositional/Properties.agda        | 10 ++++++++--
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7c43ffc092..dadc799b0e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -157,6 +157,11 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  concatMap⁺ : ∀ (f : A → List B) → xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
+  ```
+
 * In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
   ```agda
   Sublist-[]-universal : Universal (Sublist R [])
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
index 75e1a5b00a..6877c83389 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -10,8 +10,8 @@ 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⁺)
@@ -179,6 +179,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
 

From 0a89c7aab975efcdaaa2b36219df47f96a869e8c Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Fri, 5 Jul 2024 18:22:06 +0100
Subject: [PATCH 05/13] Lists: memberhsip lemma for AllPairs

---
 CHANGELOG.md                                        |  5 +++++
 .../List/Membership/Propositional/Properties.agda   | 13 +++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index dadc799b0e..12a9bfa34d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -129,6 +129,11 @@ Additions to existing modules
   All-∉-swap :  All (_∉ ys) xs → All (_∉ xs) ys
   ```
 
+* In `Data.List.Membership.Propositional.Properties`:
+  ```agda
+  ∈-AllPairs₂ : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
+  ```
+
 * In `Data.List.Membership.Propositional.Properties.WithK`:
   ```agda
   unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 03e31d8aae..a73b049d88 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -401,3 +401,16 @@ 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∈

From 7224fa09c753add30346783eaa8cb9edb0e60362 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Thu, 5 Sep 2024 13:07:15 +0100
Subject: [PATCH 06/13] =?UTF-8?q?Lists:=20membership=20lemmas=20for=20map?=
 =?UTF-8?q?=E2=88=98filter?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                                  | 12 +++++--
 .../Membership/Propositional/Properties.agda  | 15 ++++++++-
 .../List/Membership/Setoid/Properties.agda    | 31 +++++++++++++++++--
 3 files changed, 52 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 12a9bfa34d..1ae17e0fa6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -125,13 +125,19 @@ 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)
   ```
 
 * In `Data.List.Membership.Propositional.Properties`:
   ```agda
-  ∈-AllPairs₂ : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
+  ∈-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)
   ```
 
 * In `Data.List.Membership.Propositional.Properties.WithK`:
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index a73b049d88..6e9e331997 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -24,7 +24,7 @@ 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)
 open import Data.Product.Properties using (×-≡,≡↔≡)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
@@ -252,6 +252,19 @@ module _ {p} {P : A → Set p} (P? : Decidable P) where
   ∈-filter⁻ : ∀ {v xs} → 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
 
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 76bbd8beaf..f5634784f8 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -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↔)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_; _Preserves_⟶_)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
@@ -363,6 +363,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 (S₁ .Carrier) p} (P? : Decidable P) (resp : P Respects (S₁ .Setoid._≈_))
+  {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
 

From 7689668d3e1068d160ef92268e294a63584a7bf8 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Thu, 5 Sep 2024 13:56:04 +0100
Subject: [PATCH 07/13] Lists: lemmas about concatMap

---
 CHANGELOG.md                                    | 17 ++++++++++++++---
 .../Membership/Propositional/Properties.agda    | 13 +++++++++++++
 src/Data/List/Membership/Setoid/Properties.agda | 15 +++++++++++++++
 src/Data/List/Properties.agda                   |  8 ++++++++
 .../List/Relation/Unary/Any/Properties.agda     | 11 +++++++++++
 5 files changed, 61 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1ae17e0fa6..ae14b06b53 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -131,6 +131,8 @@ Additions to existing modules
   ∈-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
   ```
 
 * In `Data.List.Membership.Propositional.Properties`:
@@ -138,6 +140,8 @@ Additions to existing modules
   ∈-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
   ```
 
 * In `Data.List.Membership.Propositional.Properties.WithK`:
@@ -147,8 +151,9 @@ Additions to existing modules
 
 * 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`:
@@ -156,6 +161,12 @@ 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.Binary.Equality.Setoid`:
   ```agda
   ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
@@ -170,7 +181,7 @@ Additions to existing modules
 
 * In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
   ```agda
-  concatMap⁺ : ∀ (f : A → List B) → xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
+  concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
   ```
 
 * In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 6e9e331997..e0db425070 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -160,6 +160,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
 
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index f5634784f8..50eecde669 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -239,6 +239,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
 
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/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
 

From 3a64d8eb1321565a9be40da28122ba7d3111371c Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Fri, 6 Sep 2024 18:05:47 +0300
Subject: [PATCH 08/13] Lists: lemmas about deduplicate

---
 CHANGELOG.md                                  | 24 +++++++
 .../Membership/Propositional/Properties.agda  |  5 +-
 .../Disjoint/Propositional/Properties.agda    | 70 +++++++++++++++++++
 .../Binary/Disjoint/Setoid/Properties.agda    | 54 +++++++++-----
 .../Propositional/Properties/WithK.agda       | 62 ++++++++++++++++
 5 files changed, 195 insertions(+), 20 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 ae14b06b53..3a348bab82 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
 -----------------------------
 
@@ -142,6 +147,7 @@ Additions to existing modules
   ∈-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)
   ```
 
 * In `Data.List.Membership.Propositional.Properties.WithK`:
@@ -194,6 +200,24 @@ Additions to existing modules
   []⊆-universal : Universal ([] ⊆_)
   ```
 
+* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
+  ```agda
+  deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
+  ```
+
+* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
+  ```agda
+  deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
+  ```
+
+* 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 e0db425070..e26935aef4 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -33,7 +33,7 @@ open import Effect.Monad using (RawMonad)
 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)
@@ -123,6 +123,9 @@ module _ {v : A} where
   ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
   ∈-++⁻ = Membership.∈-++⁻ (≡.setoid A)
 
+  ∈-++ : ∀ {xs ys} → v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  ∈-++ = mk⇔ (∈-++⁻ _) Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ]
+
   ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys
   ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl
 
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..0b245332fe
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
@@ -0,0 +1,70 @@
+------------------------------------------------------------------------
+-- 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
+    private dedup≡ = deduplicate _≟_
+
+    deduplicate⁺ : Disjoint xs ys → Disjoint (dedup≡ xs) (dedup≡ ys)
+    deduplicate⁺ = S.deduplicate⁺ Sᴬ _≟_
+
+    ∈-dedup : x ∈ xs ⇔ x ∈ dedup≡ xs
+    ∈-dedup = S.∈-dedup 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..1380dd6bf3 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
@@ -8,49 +8,65 @@
 
 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
   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
+
+    open import Data.List.Membership.Setoid S using (_∈_)
+
+    private
+      dedup≡   = deduplicate _≟_
+      ∈-dedup⁺ = Mem.∈-deduplicate⁺ S _≟_
+      ∈-dedup⁻ = Mem.∈-deduplicate⁻ S _≟_
+
+    deduplicate⁺ : ∀ {xs ys} → Disjoint S xs ys → Disjoint S (dedup≡ xs) (dedup≡ ys)
+    deduplicate⁺ = _∘ Product.map (∈-dedup⁻ _) (∈-dedup⁻ _)
+
+    ∈-dedup : ∀ {x xs} → x ∈ xs ⇔ x ∈ dedup≡ xs
+    ∈-dedup = mk⇔ (∈-dedup⁺ λ where _≡_.refl x≈ → x≈) (∈-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..4f04d9cadd
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
@@ -0,0 +1,62 @@
+------------------------------------------------------------------------
+-- 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⁺; ∈-dedup)
+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≡ = ∈-dedup     _≟_
+
+  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

From d888195ab27517a814445c68344d8024f883f8ca Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Mon, 9 Sep 2024 17:33:21 +0300
Subject: [PATCH 09/13] Lists: membership lemmas about nested lists

---
 CHANGELOG.md                                  |  4 ++
 .../Membership/Propositional/Properties.agda  | 66 +++++++++++++------
 2 files changed, 50 insertions(+), 20 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3a348bab82..9b8ee29eb8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -148,6 +148,10 @@ Additions to existing modules
   ∈-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
   ```
 
 * In `Data.List.Membership.Propositional.Properties.WithK`:
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index e26935aef4..a692b7a4a2 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -10,6 +10,7 @@ module Data.List.Membership.Propositional.Properties where
 
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions using (Selective)
+open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List
 open import Data.List.Effectful using (monad)
@@ -24,13 +25,13 @@ 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 (∃; ∃₂; _×_; _,_; ∃-syntax)
+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; _⇔_; mk⇔)
@@ -40,7 +41,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_)
+  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_; subst)
 open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
 open import Relation.Nullary.Decidable.Core
@@ -55,6 +56,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 +68,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 +100,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 +118,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,13 +127,13 @@ module _ {v : A} where
   ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
   ∈-++⁻ = Membership.∈-++⁻ (≡.setoid A)
 
-  ∈-++ : ∀ {xs ys} → v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  ∈-++ : 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
@@ -139,7 +143,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
@@ -154,8 +158,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↔ ⟩
@@ -262,10 +265,10 @@ 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)
 
 ------------------------------------------------------------------------
@@ -339,13 +342,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
 
 ------------------------------------------------------------------------
@@ -366,7 +369,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
 
 ------------------------------------------------------------------------
@@ -443,3 +446,26 @@ module _ {R : A → A → Set ℓ} where
   ∈-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∈) = ⊥-elim ([]∉map∷ xs∈)
+map∷-decomp {xs = x ∷ xs} {xss = _  ∷ _} (there xs∈) =
+  let eq , p = map∷-decomp∈ xs∈
+  in -, there p , subst (λ ◆ → ◆ ∷ _ ≡ _) eq refl
+
+∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs
+∈-map∷⁻ {xss = _ ∷ _} = λ where
+  (here refl) → here refl
+  (there p)   → ∈-map∷⁻ p

From c60e8841f3442a57662eb3f58c60a6310c10f0ae Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Mon, 9 Sep 2024 18:00:34 +0300
Subject: [PATCH 10/13] =?UTF-8?q?Lists:=20extra=20subset=20lemmas=20about?=
 =?UTF-8?q?=20=5F=E2=88=B7=5F?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                                  | 16 ++++++++
 .../Propositional/Properties/Core.agda        |  8 +++-
 .../List/Membership/Setoid/Properties.agda    | 12 +++++-
 .../Subset/Propositional/Properties.agda      | 20 ++++++++--
 .../Binary/Subset/Setoid/Properties.agda      | 37 +++++++++++++++++--
 5 files changed, 84 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9b8ee29eb8..4680a9bc6a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -138,6 +138,7 @@ Additions to existing modules
                   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 ∉ []
   ```
 
 * In `Data.List.Membership.Propositional.Properties`:
@@ -152,6 +153,7 @@ Additions to existing modules
   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 ∉ []
   ```
 
 * In `Data.List.Membership.Propositional.Properties.WithK`:
@@ -216,6 +218,20 @@ Additions to existing modules
   ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
+  ```agda
+  ⊈[]    : x ∷ xs ⊈ []
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
+  ```agda
+  ⊈[]    : x ∷ xs ⊈ []
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
+  ```
+
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
   ```agda
   dedup-++-↭ : Disjoint xs ys →
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/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 50eecde669..de8e023cad 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
@@ -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
 
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
index 6877c83389..d369300df5 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -11,18 +11,18 @@ module Data.List.Relation.Binary.Subset.Propositional.Properties
 
 open import Data.Bool.Base using (Bool; true; false; T)
 open import Data.List.Base
-  using (List; map; _∷_; _++_; concat; concatMap; applyUpTo; any; filter)
+  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
@@ -52,8 +52,16 @@ 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 _)
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -150,6 +158,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 _)
+
+∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
+∈∷∧⊆⇒∈ = Subset.∈∷∧⊆⇒∈ (setoid _)
+
 ------------------------------------------------------------------------
 -- _++_
 
diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index 0d0d685a27..47661bb54e 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
@@ -9,6 +9,7 @@
 module Data.List.Relation.Binary.Subset.Setoid.Properties where
 
 open import Data.Bool.Base using (Bool; true; false)
+open import Data.Empty using (⊥-elim)
 open import Data.List.Base hiding (_∷ʳ_; find)
 import Data.List.Properties as List
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
@@ -22,7 +23,7 @@ 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 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)
@@ -41,6 +42,18 @@ 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)
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -161,12 +174,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 +189,28 @@ 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∉ x∈ = case xs⊆ x∈ of λ where
+    (here x≈) → ⊥-elim $ y∉ (∈-resp-≈ S x≈ x∈)
+    (there p) → p
+
+  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
+  ∈∷∧⊆⇒∈ = λ where
+    (here x≡y) _   → here x≡y
+    (there x∈) xs⊆ → there $ xs⊆ x∈
+
 ------------------------------------------------------------------------
 -- ++
 

From e614c2a72a6722df86872b47472dd541d66efcce Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Mon, 9 Sep 2024 18:25:20 +0300
Subject: [PATCH 11/13] =?UTF-8?q?Lists:=20extra=20lemmas=20about=20=5F?=
 =?UTF-8?q?=E2=88=B7=5F/Unique?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                                  | 12 ++++++++++
 .../Unique/Propositional/Properties.agda      | 21 +++++++++++++++---
 .../Unary/Unique/Setoid/Properties.agda       | 22 ++++++++++++++++++-
 3 files changed, 51 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4680a9bc6a..3574dd7717 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -179,6 +179,18 @@ Additions to existing modules
   concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
   ```
 
+* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
+  ```agda
+  Unique-dropSnd    : Unique S (x ∷ y ∷ xs) → Unique S (x ∷ xs)
+  Unique∷⇒head∉tail : Unique S (x ∷ xs) → x ∉ xs
+  ```
+
+* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
+  ```agda
+  Unique-dropSnd    : Unique (x ∷ y ∷ xs) → Unique (x ∷ xs)
+  Unique∷⇒head∉tail : Unique (x ∷ xs) → x ∉ xs
+  ```
+
 * In `Data.List.Relation.Binary.Equality.Setoid`:
   ```agda
   ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
index bcd7df1176..bc156a586b 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,12 @@ 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-dropSnd : Unique (x ∷ y ∷ xs) → Unique (x ∷ xs)
+Unique-dropSnd = Setoid.Unique-dropSnd (setoid _)
+
+Unique∷⇒head∉tail : Unique (x ∷ xs) → x ∉ xs
+Unique∷⇒head∉tail = Setoid.Unique∷⇒head∉tail (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..cd63b74db5 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
@@ -9,12 +9,14 @@
 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)
+open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; _∷_)
 open import Data.List.Relation.Unary.Unique.Setoid
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
@@ -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-dropSnd : Unique S (x ∷ y ∷ xs) → Unique S (x ∷ xs)
+  Unique-dropSnd ((_ ∷ x∉) ∷ uniq) = x∉ AllPairs.∷ drop⁺ S 1 uniq
+
+  Unique∷⇒head∉tail : Unique S (x ∷ xs) → x ∉ xs
+  Unique∷⇒head∉tail uniq@((x∉ ∷ _) ∷ _) = λ where
+    (here x≈)  → x∉ x≈
+    (there x∈) → Unique∷⇒head∉tail (Unique-dropSnd uniq) x∈

From 49496df000dcaec5beb735924e430ccda7d1961a Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Mon, 16 Sep 2024 14:13:12 +0100
Subject: [PATCH 12/13] Lists: incorporate feedback from James

---
 CHANGELOG.md                                  | 39 ++++++++-----------
 src/Data/List/Base.agda                       |  6 ---
 .../Membership/Propositional/Properties.agda  |  9 ++---
 .../List/Membership/Setoid/Properties.agda    |  3 +-
 .../Binary/Disjoint/Setoid/Properties.agda    |  4 +-
 .../Propositional/Properties/WithK.agda       |  2 +-
 .../Subset/Propositional/Properties.agda      | 15 ++++---
 .../Binary/Subset/Setoid/Properties.agda      | 30 ++++++++------
 .../Unique/Propositional/Properties.agda      |  7 +---
 .../Unary/Unique/Setoid/Properties.agda       | 20 +++++-----
 10 files changed, 64 insertions(+), 71 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3574dd7717..a023199f67 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,11 +123,6 @@ Additions to existing modules
   Env = Vec Carrier
  ```
 
-* In `Data.List.Base`:
-  ```agda
-  lookupMaybe : List A → ℕ → Maybe A
-  ```
-
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
   Any-∈-swap    :  Any (_∈ ys) xs → Any (_∈ xs) ys
@@ -181,14 +176,12 @@ Additions to existing modules
 
 * In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
   ```agda
-  Unique-dropSnd    : Unique S (x ∷ y ∷ xs) → Unique S (x ∷ xs)
-  Unique∷⇒head∉tail : Unique S (x ∷ xs) → x ∉ xs
+  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
   ```
 
 * In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
   ```agda
-  Unique-dropSnd    : Unique (x ∷ y ∷ xs) → Unique (x ∷ xs)
-  Unique∷⇒head∉tail : Unique (x ∷ xs) → x ∉ xs
+  Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
   ```
 
 * In `Data.List.Relation.Binary.Equality.Setoid`:
@@ -203,6 +196,20 @@ 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
@@ -230,20 +237,6 @@ Additions to existing modules
   ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
   ```
 
-* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
-  ```agda
-  ⊈[]    : x ∷ xs ⊈ []
-  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
-  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
-  ```agda
-  ⊈[]    : x ∷ xs ⊈ []
-  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
-  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
-  ```
-
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
   ```agda
   dedup-++-↭ : Disjoint xs ys →
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 3bc51ec307..0c63e34940 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -229,12 +229,6 @@ lookup : ∀ (xs : List A) → Fin (length xs) → A
 lookup (x ∷ xs) zero    = x
 lookup (x ∷ xs) (suc i) = lookup xs i
 
-lookupMaybe : List A → ℕ → Maybe A
-lookupMaybe = λ where
-  []       _       → nothing
-  (x ∷ _)  zero    → just x
-  (_ ∷ xs) (suc n) → lookupMaybe xs n
-
 -- Numerical
 
 upTo : ℕ → List ℕ
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index a692b7a4a2..2a8af5bc27 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -10,7 +10,6 @@ module Data.List.Membership.Propositional.Properties where
 
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions using (Selective)
-open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List
 open import Data.List.Effectful using (monad)
@@ -41,7 +40,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_; subst)
+  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
 open import Relation.Nullary.Decidable.Core
@@ -107,7 +106,7 @@ module _ (f : A → B) where
   ∈-map⁻ = Membership.∈-map⁻ (≡.setoid A) (≡.setoid B)
 
   map-∈↔ : (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs
-  map-∈↔ {xs}{y} =
+  map-∈↔ {xs} {y} =
     (∃ λ x → x ∈ xs × y ≡ f x)   ↔⟨ Any↔ ⟩
     Any (λ x → y ≡ f x) xs       ↔⟨ map↔ ⟩
     y ∈ List.map f xs            ∎
@@ -460,10 +459,10 @@ map∷-decomp∈ {xss = _ ∷ _} = λ where
 
 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∈) = ⊥-elim ([]∉map∷ xs∈)
+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 , subst (λ ◆ → ◆ ∷ _ ≡ _) eq refl
+  in -, there p , cong (_∷ _) (sym eq)
 
 ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs
 ∈-map∷⁻ {xss = _ ∷ _} = λ where
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index de8e023cad..4ee33d14c4 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -393,7 +393,7 @@ module _ (S : Setoid c ℓ) {P : Pred (Carrier S) p}
 
 module _
   (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂)
-  {P : Pred (S₁ .Carrier) p} (P? : Decidable P) (resp : P Respects (S₁ .Setoid._≈_))
+  {P : Pred _ p} (P? : Decidable P) (resp : P Respects _)
   {f xs y} where
 
   open Setoid     S₁ renaming (_≈_ to _≈₁_)
@@ -513,4 +513,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/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
index 1380dd6bf3..8178579d39 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
@@ -26,7 +26,7 @@ open import Relation.Nullary.Negation using (¬_)
 
 module _ {c ℓ} (S : Setoid c ℓ) where
 
-  open Setoid S using (_≈_; reflexive) renaming (Carrier to A)
+  open Setoid S using (_≉_; reflexive) renaming (Carrier to A)
 
   ------------------------------------------------------------------------
   -- Relational properties
@@ -40,7 +40,7 @@ module _ {c ℓ} (S : Setoid c ℓ) where
   ------------------------------------------------------------------------
 
   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)))
 
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
index 4f04d9cadd..16f080fbfe 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
@@ -33,7 +33,7 @@ open import Relation.Binary.Definitions using (DecidableEquality)
 ------------------------------------------------------------------------
 -- deduplicate
 
-module _ {a}{A : Set a} (_≟_ : DecidableEquality A) where
+module _ {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
   private
     dedup≡   = deduplicate _≟_
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
index d369300df5..4054afc092 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -28,7 +28,7 @@ open import Data.List.Relation.Binary.Permutation.Propositional
 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)
@@ -59,8 +59,11 @@ private
 -- Basics
 ------------------------------------------------------------------------
 
-⊈[] : x ∷ xs ⊈ []
-⊈[] = Subset.⊈[] (setoid _)
+∷⊈[] : x ∷ xs ⊈ []
+∷⊈[] = Subset.∷⊈[] (setoid _)
+
+⊆[]⇒≡[] : ∀ {A : Set a} → (_⊆ []) ⋐ (_≡ [])
+⊆[]⇒≡[] {A = A} = Subset.⊆[]⇒≡[] (setoid A)
 
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
@@ -158,12 +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 _)
 
-∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
-∈∷∧⊆⇒∈ = Subset.∈∷∧⊆⇒∈ (setoid _)
-
 ------------------------------------------------------------------------
 -- _++_
 
diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index 47661bb54e..901ee8b942 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
@@ -9,7 +9,6 @@
 module Data.List.Relation.Binary.Subset.Setoid.Properties where
 
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Empty using (⊥-elim)
 open import Data.List.Base hiding (_∷ʳ_; find)
 import Data.List.Properties as List
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
@@ -23,6 +22,7 @@ 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 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)
@@ -35,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)
 
@@ -51,8 +52,12 @@ module _ (S : Setoid a ℓ) where
   open Setoid S using (refl)
   open Subset S
 
-  ⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
-  ⊈[] p = Membershipₚ.∉[] S $ p (here refl)
+  ∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
+  ∷⊈[] p = Membershipₚ.∉[] S $ p (here refl)
+
+  ⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ [])
+  ⊆[]⇒≡[] {x = []}    _ = ≡.refl
+  ⊆[]⇒≡[] {x = _ ∷ _} p with () ← ∷⊈[] p
 
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
@@ -201,15 +206,18 @@ module _ (S : Setoid a ℓ) where
   ∈-∷⁺ʳ 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∉ x∈ = case xs⊆ x∈ of λ where
-    (here x≈) → ⊥-elim $ y∉ (∈-resp-≈ S x≈ x∈)
-    (there p) → p
-
-  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
-  ∈∷∧⊆⇒∈ = λ where
-    (here x≡y) _   → here x≡y
-    (there x∈) xs⊆ → there $ xs⊆ x∈
+  ⊆∷∧∉⇒⊆ 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/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
index bc156a586b..8852bdd704 100644
--- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
@@ -164,8 +164,5 @@ module _ {A : Set a} {P : Pred _ p} (P? : Decidable P) where
 ------------------------------------------------------------------------
 -- ∷
 
-Unique-dropSnd : Unique (x ∷ y ∷ xs) → Unique (x ∷ xs)
-Unique-dropSnd = Setoid.Unique-dropSnd (setoid _)
-
-Unique∷⇒head∉tail : Unique (x ∷ xs) → x ∉ xs
-Unique∷⇒head∉tail = Setoid.Unique∷⇒head∉tail (setoid _)
+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 cd63b74db5..0dc7027c79 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
@@ -16,7 +16,7 @@ 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; _∷_)
+open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
 open import Data.List.Relation.Unary.Unique.Setoid
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
@@ -165,14 +165,14 @@ module _ (S : Setoid a ℓ) {P : Pred _ p} (P? : Decidable P) where
 module _ (S : Setoid a ℓ) where
 
   open Setoid S renaming (Carrier to A)
-  open Membership S using (_∈_; _∉_)
+  open Membership S using (_∉_)
 
-  private variable x y : A; xs : List A
+  private
+    variable
+      x y : A
+      xs : List A
 
-  Unique-dropSnd : Unique S (x ∷ y ∷ xs) → Unique S (x ∷ xs)
-  Unique-dropSnd ((_ ∷ x∉) ∷ uniq) = x∉ AllPairs.∷ drop⁺ S 1 uniq
-
-  Unique∷⇒head∉tail : Unique S (x ∷ xs) → x ∉ xs
-  Unique∷⇒head∉tail uniq@((x∉ ∷ _) ∷ _) = λ where
-    (here x≈)  → x∉ x≈
-    (there x∈) → Unique∷⇒head∉tail (Unique-dropSnd uniq) x∈
+  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∈

From 0d54dec7feed51801008dd4eded706ab670882bb Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Mon, 16 Sep 2024 21:08:45 +0100
Subject: [PATCH 13/13] Lists: incorporate feedback from Guillaume

---
 CHANGELOG.md                                  | 44 +++++++++----------
 .../Membership/Propositional/Properties.agda  | 11 +++--
 .../List/Membership/Setoid/Properties.agda    | 12 +++--
 .../Disjoint/Propositional/Properties.agda    |  7 +--
 .../Binary/Disjoint/Setoid/Properties.agda    | 16 ++-----
 .../Propositional/Properties/WithK.agda       | 32 +++++---------
 6 files changed, 55 insertions(+), 67 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a023199f67..a513e4978f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -125,30 +125,32 @@ 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
-  ∈-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 ∉ []
+  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 ∉ []
+  ∈-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`:
@@ -228,13 +230,11 @@ Additions to existing modules
 * In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
   ```agda
   deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
-  ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
   ```
 
 * In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
   ```agda
   deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
-  ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 2a8af5bc27..39204f19e2 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -126,8 +126,8 @@ 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.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ]
+  ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  ++-∈⇔ = mk⇔ (∈-++⁻ _) Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ]
 
   ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys
   ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl
@@ -299,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≈
 
 ------------------------------------------------------------------------
 -- _>>=_
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 4ee33d14c4..c17fa15b98 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -25,7 +25,7 @@ open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂; ∃-syn
 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 (_↔_; mk↔)
+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)
@@ -426,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
 
diff --git a/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
index 0b245332fe..b2b2ec591c 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
@@ -61,10 +61,5 @@ module _ {a} {A : Set a} where
 
   -- deduplicate
   module _ (_≟_ : DecidableEquality A) where
-    private dedup≡ = deduplicate _≟_
-
-    deduplicate⁺ : Disjoint xs ys → Disjoint (dedup≡ xs) (dedup≡ ys)
+    deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
     deduplicate⁺ = S.deduplicate⁺ Sᴬ _≟_
-
-    ∈-dedup : x ∈ xs ⇔ x ∈ dedup≡ xs
-    ∈-dedup = S.∈-dedup Sᴬ _≟_
diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
index 8178579d39..3416fc31e8 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
@@ -58,15 +58,7 @@ module _ {c ℓ} (S : Setoid c ℓ) where
   -- deduplicate
   module _ (_≟_ : DecidableEquality A) where
 
-    open import Data.List.Membership.Setoid S using (_∈_)
-
-    private
-      dedup≡   = deduplicate _≟_
-      ∈-dedup⁺ = Mem.∈-deduplicate⁺ S _≟_
-      ∈-dedup⁻ = Mem.∈-deduplicate⁻ S _≟_
-
-    deduplicate⁺ : ∀ {xs ys} → Disjoint S xs ys → Disjoint S (dedup≡ xs) (dedup≡ ys)
-    deduplicate⁺ = _∘ Product.map (∈-dedup⁻ _) (∈-dedup⁻ _)
-
-    ∈-dedup : ∀ {x xs} → x ∈ xs ⇔ x ∈ dedup≡ xs
-    ∈-dedup = mk⇔ (∈-dedup⁺ λ where _≡_.refl x≈ → x≈) (∈-dedup⁻ _)
+    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
index 16f080fbfe..3bed7656fc 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
@@ -14,14 +14,12 @@ open import Function.Related.Propositional using (SK-sym; module EquationalReaso
 
 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.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⁺; ∈-dedup)
+  using (deduplicate⁺)
 open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
 open import Data.List.Relation.Binary.BagAndSetEquality using (∼bag⇒↭)
 
@@ -36,27 +34,21 @@ open import Relation.Binary.Definitions using (DecidableEquality)
 module _ {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
   private
-    dedup≡   = deduplicate _≟_
-    ∈-dedup≡ = ∈-dedup     _≟_
+    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
+  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
+    λ {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