From 9556a7bc63d18e8b5c62c9848c7a3d54a0604f4c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 10:38:13 +0000
Subject: [PATCH 01/13] refactor: prepare for code migration

---
 CHANGELOG.md                                     | 2 +-
 src/Data/List/Relation/Unary/All/Properties.agda | 9 +++------
 2 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e7b6c94d5e..2cb9c50f1e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -327,11 +327,11 @@ Additions to existing modules
 * In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
   ```agda
   ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
+  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
-  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
   all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
   all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs
   ```
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 7662c4cea1..c557532fee 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -20,9 +20,6 @@ import Data.List.Membership.Setoid as SetoidMembership
 import Data.List.Properties as List
 import Data.List.Relation.Binary.Equality.Setoid as ≋
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
-import Data.List.Relation.Binary.Sublist.Propositional as Sublist
-import Data.List.Relation.Binary.Sublist.Propositional.Properties
-  as Sublist
 import Data.List.Relation.Binary.Subset.Propositional as Subset
 open import Data.List.Relation.Unary.All as All using
   ( All; []; _∷_; lookup; updateAt
@@ -49,7 +46,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
 open import Relation.Unary
-  using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
+  using (Decidable; Pred; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)
 
 private
@@ -387,12 +384,12 @@ concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)
 concat⁻ : ∀ {xss} → All P (concat xss) → All (All P) xss
 concat⁻ {xss = []}       []  = []
 concat⁻ {xss = xs ∷ xss} pxs = ++⁻ˡ xs pxs ∷ concat⁻ (++⁻ʳ xs pxs)
-
+{-
 all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
 all⊆concat [] = []
 all⊆concat (xs ∷ xss) =
   Sublist.++⁺ʳ (concat xss) Sublist.⊆-refl ∷ All.map (Sublist.++⁺ˡ xs) (all⊆concat xss)
-
+-}
 ------------------------------------------------------------------------
 -- snoc
 

From 40a12970b95dda9fd57c72e3929f6a85ac30e815 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 13:10:48 +0000
Subject: [PATCH 02/13] refactor: move code as is

---
 .../Binary/Sublist/Propositional/Properties.agda     | 12 ++++++++++--
 src/Data/List/Relation/Unary/All/Properties.agda     |  7 +------
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
index dbe82f1949..75e97df2c9 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
@@ -8,9 +8,9 @@
 
 module Data.List.Relation.Binary.Sublist.Propositional.Properties where
 
-open import Data.List.Base using (List; []; _∷_;  map)
+open import Data.List.Base using (List; []; _∷_;  map; concat)
 open import Data.List.Membership.Propositional using (_∈_)
-open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.Any.Properties
   using (here-injective; there-injective)
@@ -63,6 +63,14 @@ module _ (S : Setoid a ℓ) where
 map⁺ : (f : A → B) → xs ⊆ ys → map f xs ⊆ map f ys
 map⁺ f = SetoidProperties.map⁺ (setoid _) (setoid _) (cong f)
 
+------------------------------------------------------------------------
+-- concat
+
+all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
+all⊆concat [] = []
+all⊆concat (xs ∷ xss) =
+  ++⁺ʳ (concat xss) ⊆-refl ∷ All.map (++⁺ˡ xs) (all⊆concat xss)
+
 ------------------------------------------------------------------------
 -- Category laws for _⊆_
 
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index c557532fee..fd30adc42b 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -384,12 +384,7 @@ concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)
 concat⁻ : ∀ {xss} → All P (concat xss) → All (All P) xss
 concat⁻ {xss = []}       []  = []
 concat⁻ {xss = xs ∷ xss} pxs = ++⁻ˡ xs pxs ∷ concat⁻ (++⁻ʳ xs pxs)
-{-
-all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
-all⊆concat [] = []
-all⊆concat (xs ∷ xss) =
-  Sublist.++⁺ʳ (concat xss) Sublist.⊆-refl ∷ All.map (Sublist.++⁺ˡ xs) (all⊆concat xss)
--}
+
 ------------------------------------------------------------------------
 -- snoc
 

From 4cbdb68e90eb307c03067eb61b1cab3fdd9eb17b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 17:53:11 +0000
Subject: [PATCH 03/13] refactor: add new lemmas to `Setoid` and
 `Propositional`

---
 CHANGELOG.md                                          |  6 ++++++
 .../Binary/Sublist/Propositional/Properties.agda      | 10 +++++++++-
 .../Relation/Binary/Sublist/Setoid/Properties.agda    | 11 +++++++++++
 3 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2cb9c50f1e..d4ac934317 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -327,9 +327,15 @@ Additions to existing modules
 * In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
   ```agda
   ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
+  xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
   all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
   ```
 
+* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
+  ```agda
+  concat⁺ : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
index 75e97df2c9..a8141d19dc 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
@@ -10,11 +10,12 @@ module Data.List.Relation.Binary.Sublist.Propositional.Properties where
 
 open import Data.List.Base using (List; []; _∷_;  map; concat)
 open import Data.List.Membership.Propositional using (_∈_)
+import Data.List.Properties as List
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.Any.Properties
   using (here-injective; there-injective)
-open import Data.List.Relation.Binary.Sublist.Propositional
+open import Data.List.Relation.Binary.Sublist.Propositional as Propositional
   hiding (map)
 import Data.List.Relation.Binary.Sublist.Setoid
   as SetoidSublist
@@ -37,6 +38,7 @@ private
     A B : Set a
     x y : A
     ws xs ys zs : List A
+    xss : List A
 
 ------------------------------------------------------------------------
 -- Re-exporting setoid properties
@@ -66,6 +68,12 @@ map⁺ f = SetoidProperties.map⁺ (setoid _) (setoid _) (cong f)
 ------------------------------------------------------------------------
 -- concat
 
+xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
+xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
+  with prf ← concat⁺ (Propositional.map ⊆-reflexive (from∈ xs∈xss))
+  rewrite List.++-identityʳ xs
+  = prf
+
 all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
 all⊆concat [] = []
 all⊆concat (xs ∷ xss) =
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index b42e33365d..b6c82388e6 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -30,6 +30,8 @@ open import Relation.Nullary.Decidable using (¬?; yes; no)
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
+import Data.List.Relation.Binary.Sublist.Heterogeneous
+  as Hetero
 import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
   as HeteroProperties
 import Data.List.Membership.Setoid as SetoidMembership
@@ -44,6 +46,7 @@ private
     p q r s t : Level
     a b x y : A
     as bs cs ds xs ys : List A
+    ass bss xss yss : List (List A)
     P : Pred A p
     Q : Pred A q
     m n : ℕ
@@ -175,6 +178,14 @@ module _ where
   ++⁻ : length as ≡ length bs → as ++ cs ⊆ bs ++ ds → cs ⊆ ds
   ++⁻ = HeteroProperties.++⁻
 
+------------------------------------------------------------------------
+-- concat
+
+  concat⁺ : Hetero.Sublist _⊆_ ass bss →
+            concat ass ⊆ concat bss
+  concat⁺ = HeteroProperties.concat⁺
+
+
 ------------------------------------------------------------------------
 -- take
 

From 1f0e8cdef3dbb12b31634fd6a1926a6d54700970 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 17:58:08 +0000
Subject: [PATCH 04/13] refactor: use new lemmas

---
 .../Relation/Binary/Sublist/Propositional/Properties.agda     | 4 +---
 src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda  | 1 -
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
index a8141d19dc..828df4c1a5 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
@@ -75,9 +75,7 @@ xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
   = prf
 
 all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
-all⊆concat [] = []
-all⊆concat (xs ∷ xss) =
-  ++⁺ʳ (concat xss) ⊆-refl ∷ All.map (++⁺ˡ xs) (all⊆concat xss)
+all⊆concat _ = All.tabulate xs∈xss⇒xs⊆concat[xss]
 
 ------------------------------------------------------------------------
 -- Category laws for _⊆_
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index b6c82388e6..94380adf8f 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -185,7 +185,6 @@ module _ where
             concat ass ⊆ concat bss
   concat⁺ = HeteroProperties.concat⁺
 
-
 ------------------------------------------------------------------------
 -- take
 

From 829fc88acd892eebd7da46dde340816d308a2ce2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 18:17:57 +0000
Subject: [PATCH 05/13] refactor: localise appeals to `SetoidMembership`; pull
 lemma back to `SetoidProperties`

---
 .../Binary/Sublist/Setoid/Properties.agda     | 26 +++++++++++++++----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index 94380adf8f..d94e2707d9 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -13,6 +13,7 @@ module Data.List.Relation.Binary.Sublist.Setoid.Properties
   {c ℓ} (S : Setoid c ℓ) where
 
 open import Data.List.Base hiding (_∷ʳ_)
+open import Data.List.Properties using (++-identityʳ)
 open import Data.List.Relation.Unary.Any using (Any)
 import Data.Maybe.Relation.Unary.All as Maybe
 open import Data.Nat.Base using (ℕ; _≤_; _≥_)
@@ -37,16 +38,16 @@ import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
 import Data.List.Membership.Setoid as SetoidMembership
 
 open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl)
-open SetoidEquality S using (_≋_; ≋-refl)
+open SetoidEquality S using (_≋_; ≋-refl; ≋-setoid)
 open SetoidSublist S hiding (map)
-open SetoidMembership S using (_∈_)
+--
 
 private
   variable
     p q r s t : Level
     a b x y : A
     as bs cs ds xs ys : List A
-    ass bss xss yss : List (List A)
+    xss yss : List (List A)
     P : Pred A p
     Q : Pred A q
     m n : ℕ
@@ -181,10 +182,23 @@ module _ where
 ------------------------------------------------------------------------
 -- concat
 
-  concat⁺ : Hetero.Sublist _⊆_ ass bss →
-            concat ass ⊆ concat bss
+module _ where
+
+  concat⁺ : Hetero.Sublist _⊆_ xss yss →
+            concat xss ⊆ concat yss
   concat⁺ = HeteroProperties.concat⁺
 
+  open SetoidMembership ≋-setoid using (_∈_)
+  open SetoidSublist ≋-setoid
+    using ()
+    renaming (map to map-≋; from∈ to from∈-≋)
+
+  xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
+  xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
+    with prf ← concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss))
+    rewrite ++-identityʳ xs
+    = prf
+
 ------------------------------------------------------------------------
 -- take
 
@@ -316,6 +330,8 @@ module _ where
 
 module _ where
 
+  open SetoidMembership S using (_∈_)
+
   to∈-injective : ∀ {p q : [ x ] ⊆ xs} → to∈ p ≡ to∈ q → p ≡ q
   to∈-injective = HeteroProperties.toAny-injective
 

From f14df96aeb28d4731d08eec6baeeae0979812bca Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 18:26:51 +0000
Subject: [PATCH 06/13] =?UTF-8?q?refactor:=20pull=20`all=E2=8A=86concat`?=
 =?UTF-8?q?=20back=20to=20`Setoid.Properties`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../List/Relation/Binary/Sublist/Setoid/Properties.agda     | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index d94e2707d9..a22beaa567 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -15,6 +15,7 @@ module Data.List.Relation.Binary.Sublist.Setoid.Properties
 open import Data.List.Base hiding (_∷ʳ_)
 open import Data.List.Properties using (++-identityʳ)
 open import Data.List.Relation.Unary.Any using (Any)
+open import Data.List.Relation.Unary.All using (All; tabulateₛ)
 import Data.Maybe.Relation.Unary.All as Maybe
 open import Data.Nat.Base using (ℕ; _≤_; _≥_)
 import Data.Nat.Properties as ℕ
@@ -40,7 +41,7 @@ import Data.List.Membership.Setoid as SetoidMembership
 open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl)
 open SetoidEquality S using (_≋_; ≋-refl; ≋-setoid)
 open SetoidSublist S hiding (map)
---
+
 
 private
   variable
@@ -199,6 +200,9 @@ module _ where
     rewrite ++-identityʳ xs
     = prf
 
+  all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
+  all⊆concat _ = tabulateₛ ≋-setoid xs∈xss⇒xs⊆concat[xss]
+
 ------------------------------------------------------------------------
 -- take
 

From 309a7b9806059fdc83066dcd2346c3d5af24e15c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 18:32:36 +0000
Subject: [PATCH 07/13] refactor: tidy up

---
 CHANGELOG.md                                     |  5 ++---
 .../Binary/Sublist/Propositional/Properties.agda | 16 ++--------------
 2 files changed, 4 insertions(+), 17 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d4ac934317..4272a70c0c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -327,13 +327,12 @@ Additions to existing modules
 * In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
   ```agda
   ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
-  xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
-  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
   ```
 
 * In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
   ```agda
-  concat⁺ : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
+  concat⁺    : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
+  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
index 828df4c1a5..ce6c9f853a 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
@@ -8,10 +8,10 @@
 
 module Data.List.Relation.Binary.Sublist.Propositional.Properties where
 
-open import Data.List.Base using (List; []; _∷_;  map; concat)
+open import Data.List.Base using (List; []; _∷_;  map)
 open import Data.List.Membership.Propositional using (_∈_)
 import Data.List.Properties as List
-open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.Any.Properties
   using (here-injective; there-injective)
@@ -65,18 +65,6 @@ module _ (S : Setoid a ℓ) where
 map⁺ : (f : A → B) → xs ⊆ ys → map f xs ⊆ map f ys
 map⁺ f = SetoidProperties.map⁺ (setoid _) (setoid _) (cong f)
 
-------------------------------------------------------------------------
--- concat
-
-xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
-xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
-  with prf ← concat⁺ (Propositional.map ⊆-reflexive (from∈ xs∈xss))
-  rewrite List.++-identityʳ xs
-  = prf
-
-all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
-all⊆concat _ = All.tabulate xs∈xss⇒xs⊆concat[xss]
-
 ------------------------------------------------------------------------
 -- Category laws for _⊆_
 

From 65e7c210afcd7f6bcef40436d2fd118e9461092f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 19:11:38 +0000
Subject: [PATCH 08/13] refactor: tidy up

---
 .../List/Relation/Binary/Sublist/Propositional/Properties.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
index ce6c9f853a..a7d73454ab 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
@@ -10,12 +10,11 @@ module Data.List.Relation.Binary.Sublist.Propositional.Properties where
 
 open import Data.List.Base using (List; []; _∷_;  map)
 open import Data.List.Membership.Propositional using (_∈_)
-import Data.List.Properties as List
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.Any.Properties
   using (here-injective; there-injective)
-open import Data.List.Relation.Binary.Sublist.Propositional as Propositional
+open import Data.List.Relation.Binary.Sublist.Propositional
   hiding (map)
 import Data.List.Relation.Binary.Sublist.Setoid
   as SetoidSublist

From 6e93979f8077b94e697448c684b47f26aea60062 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 19:14:56 +0000
Subject: [PATCH 09/13] refactor: tidy up

---
 .../List/Relation/Binary/Sublist/Propositional/Properties.agda | 1 -
 src/Data/List/Relation/Unary/All/Properties.agda               | 3 ++-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
index a7d73454ab..dbe82f1949 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
@@ -37,7 +37,6 @@ private
     A B : Set a
     x y : A
     ws xs ys zs : List A
-    xss : List A
 
 ------------------------------------------------------------------------
 -- Re-exporting setoid properties
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index fd30adc42b..a592d497c1 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -45,8 +45,9 @@ open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
+
 open import Relation.Unary
-  using (Decidable; Pred; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
+  using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)
 
 private

From 1104979e7f5719090b24b8327d95fd68385d8824 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Dec 2024 19:16:59 +0000
Subject: [PATCH 10/13] refactor: tidy up

---
 src/Data/List/Relation/Unary/All/Properties.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index a592d497c1..c5f56e2d3b 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -45,7 +45,6 @@ open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
-
 open import Relation.Unary
   using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)

From 9fd54230b2ab8336800d79c72bcd10ba85a26764 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 19 Dec 2024 09:19:58 +0000
Subject: [PATCH 11/13] refactor: make proof `rewrite`-free

---
 .../Relation/Binary/Sublist/Setoid/Properties.agda     | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index a22beaa567..6f72ef7b9d 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -24,7 +24,8 @@ open import Function.Base
 open import Function.Bundles using (_⇔_; _⤖_)
 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.PropositionalEquality.Core as ≡
+  using (_≡_; refl; sym; cong; cong₂)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
 open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant)
 open import Relation.Nullary.Negation using (¬_)
@@ -39,7 +40,7 @@ import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
 import Data.List.Membership.Setoid as SetoidMembership
 
 open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl)
-open SetoidEquality S using (_≋_; ≋-refl; ≋-setoid)
+open SetoidEquality S using (_≋_; ≋-refl; ≋-reflexive; ≋-setoid)
 open SetoidSublist S hiding (map)
 
 
@@ -196,9 +197,12 @@ module _ where
 
   xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
   xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
+{-
     with prf ← concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss))
     rewrite ++-identityʳ xs
-    = prf
+-}
+    = ⊆-trans (⊆-reflexive (≋-reflexive {!sym (++-identityʳ xs)!}))
+              (concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss)))
 
   all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
   all⊆concat _ = tabulateₛ ≋-setoid xs∈xss⇒xs⊆concat[xss]

From 9cde3557c13a7e5bc0d5757effbeb4d3754cea50 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 19 Dec 2024 09:32:12 +0000
Subject: [PATCH 12/13] oops: uncommitted file save

---
 .../List/Relation/Binary/Sublist/Setoid/Properties.agda     | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index 6f72ef7b9d..83c42164d9 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -197,11 +197,7 @@ module _ where
 
   xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
   xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
-{-
-    with prf ← concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss))
-    rewrite ++-identityʳ xs
--}
-    = ⊆-trans (⊆-reflexive (≋-reflexive {!sym (++-identityʳ xs)!}))
+    = ⊆-trans (⊆-reflexive (≋-reflexive (sym (++-identityʳ xs))))
               (concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss)))
 
   all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss

From 45ef541d4ade943f6daab47b83fb4f3e0185ea06 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 24 Dec 2024 13:25:39 +0000
Subject: [PATCH 13/13] tighten `import`s

---
 src/Data/List/Relation/Unary/All/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index c5f56e2d3b..81ee418966 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -46,7 +46,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
 open import Relation.Unary
-  using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
+  using (Decidable; Pred; ∁; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)
 
 private