diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 93c23f6fe7..56b4c88637 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -32,7 +32,7 @@ on:
 ## To be experimented with again in the future to see if things have
 ## gotten better.
 ##
-## We use `v1-install` rather than `install` as Agda as a community
+## We mostly use `v1-install` rather than `install` as Agda as a community
 ## hasn't figured out how to manage dependencies with the new local
 ## style builds (see agda/agda#4627 for details). Once this is resolved
 ## we should upgrade to `install`.
@@ -50,8 +50,8 @@ on:
 env:
   GHC_VERSION: 9.8.2
   CABAL_VERSION: 3.10.3.0
-  CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
-  # CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
+  CABAL_V1_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
+  CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
   AGDA: agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc
 
 jobs:
@@ -121,13 +121,15 @@ jobs:
           cabal-update: true
 
       - name: Put cabal programs in PATH
-        run: echo "~/.cabal/bin" >> "${GITHUB_PATH}"
+        run: echo ~/.cabal/bin >> "${GITHUB_PATH}"
 
       - name: Install alex & happy
         if: steps.cache-cabal.outputs.cache-hit != 'true'
         run: |
           ${{ env.CABAL_INSTALL }} alex
           ${{ env.CABAL_INSTALL }} happy
+          # happy>=2.0 cannot be v1-installed: https://github.com/haskell/happy/issues/315
+          # Since we only need the executable, it is fine to use v2-install here.
 
       - name: Download and install Agda from github
         if: steps.cache-cabal.outputs.cache-hit != 'true'
@@ -137,7 +139,7 @@ jobs:
           git checkout ${{ env.AGDA_COMMIT }}
           mkdir -p doc
           touch doc/user-manual.pdf
-          ${{ env.CABAL_INSTALL }}
+          ${{ env.CABAL_V1_INSTALL }}
           cd ..
 
 ########################################################################
@@ -167,7 +169,7 @@ jobs:
 
       - name: Golden testing
         run: |
-          ${{ env.CABAL_INSTALL }} clock
+          ${{ env.CABAL_V1_INSTALL }} clock
           make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda'
 
 
diff --git a/CHANGELOG.md b/CHANGELOG.md
index af16162afa..45e612b514 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -59,6 +59,13 @@ Deprecated names
   normalise-correct  ↦  Algebra.Solver.Monoid.Normal.correct
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
+  ```agda
+  split  ↦  ↭-split
+  ```
+  with a more informative type (see below).
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   ++-assoc _      ↦  ++-assoc-eqFree
@@ -98,6 +105,11 @@ New modules
   Data.List.Relation.Unary.All.Properties.Core
   ```
 
+* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
+  Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties`
+
+* `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
+
 Additions to existing modules
 -----------------------------
 
@@ -120,19 +132,62 @@ 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
+  ∉⇒All[≉]       : x ∉ xs → All (x ≉_) xs
+  All[≉]⇒∉       : All (x ≉_) xs → x ∉ xs
+  Any-∈-swap     : Any (_∈ ys) xs → Any (_∈ xs) ys
+  All-∉-swap     : All (_∉ ys) xs → All (_∉ xs) ys
+  ∈-map∘filter⁻  : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
+  ∈-map∘filter⁺  : f Preserves _≈₁_ ⟶ _≈₂_ →
+                   ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
+                   y ∈₂ map f (filter P? xs)
+  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∉[]            : x ∉ []
+  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
+  ```
+
+* In `Data.List.Membership.Propositional.Properties`:
+  ```agda
+  ∈-AllPairs₂    : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
+  ∈-map∘filter⁻  : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x)
+  ∈-map∘filter⁺  : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs)
+  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ++-∈⇔          : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  []∉map∷        : [] ∉ map (x ∷_) xss
+  map∷-decomp∈   : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
+  map∷-decomp    : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs
+  ∈-map∷⁻        : xs ∈ map (x ∷_) xss → x ∈ xs
+  ∉[]            : x ∉ []
+  deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
+  ```
+
+* In `Data.List.Membership.Propositional.Properties.WithK`:
+  ```agda
+  unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
   ```
 
 * In `Data.List.Properties`:
   ```agda
-  product≢0 : All NonZero ns → NonZero (product ns)
-  ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
+  product≢0    : All NonZero ns → NonZero (product ns)
+  ∈⇒≤product   : All NonZero ns → n ∈ ns → n ≤ product ns
+  concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
   ```
 
-* In `Data.List.Relation.Unary.All`:
+* In `Data.List.Relation.Unary.Any.Properties`:
   ```agda
-  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
+  concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
+  concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
+  ```
+
+* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
+  ```agda
+  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
+  ```
+
+* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
+  ```agda
+  Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
   ```
 
 * In `Data.List.Relation.Binary.Equality.Setoid`:
@@ -141,12 +196,105 @@ Additions to existing modules
   ++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Homogeneous`:
+  ```agda
+  steps : Permutation R xs ys → ℕ
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Propositional`:
+  constructor aliases
+  ```agda
+  ↭-refl  : Reflexive _↭_
+  ↭-prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
+  ↭-swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
+  ```
+  and properties
+  ```agda
+  ↭-reflexive-≋ : _≋_ ⇒ _↭_
+  ↭⇒↭ₛ          : _↭_  ⇒ _↭ₛ_
+  ↭ₛ⇒↭          : _↭ₛ_ ⇒ _↭_
+  ```
+  where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation`
+
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
+  ```agda
+  Any-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : Any P ys) →
+                     Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
+  ∈-resp-[σ∘σ⁻¹]   : (σ : xs ↭ ys) (iy : y ∈ ys) →
+                     ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
+  product-↭        : product Preserves _↭_ ⟶ _≡_
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Setoid`:
+  ```agda
+  ↭-reflexive-≋ : _≋_  ⇒ _↭_
+  ↭-transˡ-≋    : LeftTrans _≋_ _↭_
+  ↭-transʳ-≋    : RightTrans _↭_ _≋_
+  ↭-trans′      : Transitive _↭_
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
+  ```agda
+  ↭-split : xs ↭ (as ++ [ v ] ++ bs) →
+            ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs) × (ps ++ qs) ↭ (as ++ bs)
+  drop-∷  : x ∷ xs ↭ x ∷ ys → xs ↭ ys
+  ```
+
 * In `Data.List.Relation.Binary.Pointwise`:
   ```agda
   ++⁺ʳ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R)
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* In `Data.List.Relation.Unary.All`:
+  ```agda
+  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
+
+* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
+  ```agda
+  ∷⊈[]   : x ∷ xs ⊈ []
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ```
+
+* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  ∷⊈[]   : x ∷ xs ⊈ []
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ```
+
+* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
+  ```
+
+* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
+  ```agda
+  Sublist-[]-universal : Universal (Sublist R [])
+  ```
+
+* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
+  ```agda
+  []⊆-universal : Universal ([] ⊆_)
+  ```
+
+* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
+  ```agda
+  deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  ```
+
+* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
+  ```agda
+  deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
+  ```agda
+  dedup-++-↭ : Disjoint xs ys →
+               deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
+  ```
+
 * In `Data.Maybe.Properties`:
   ```agda
   maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
@@ -188,6 +336,17 @@ Additions to existing modules
   ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
  ```
 
+* In `Relation.Binary.Construct.Interior.Symmetric`:
+  ```agda
+  decidable         : Decidable R → Decidable (SymInterior R)
+  ```
+  and for `Reflexive` and `Transitive` relations `R`:
+  ```agda
+  isDecEquivalence  : Decidable R → IsDecEquivalence (SymInterior R)
+  isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R
+  decPoset          : Decidable R → DecPoset _ _ _
+  ```
+
 * In `Relation.Nullary.Decidable`:
   ```agda
   does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 03e31d8aae..39204f19e2 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -24,16 +24,16 @@ open import Data.List.Relation.Unary.Any.Properties
 open import Data.Nat.Base using (ℕ; suc; s≤s; _≤_; _<_; _≰_)
 open import Data.Nat.Properties
   using (suc-injective; m≤n⇒m≤1+n; _≤?_; <⇒≢; ≰⇒>)
-open import Data.Product.Base using (∃; ∃₂; _×_; _,_)
+open import Data.Product.Base using (∃; ∃₂; _×_; _,_; ∃-syntax; -,_; map₂)
 open import Data.Product.Properties using (×-≡,≡↔≡)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Effect.Monad using (RawMonad)
-open import Function.Base using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_)
+open import Function.Base using (_∘_; _∘′_; _$_; id; flip; _⟨_⟩_; _∋_)
 open import Function.Definitions using (Injective)
 import Function.Related.Propositional as Related
-open import Function.Bundles using (_↔_; _↣_; Injection)
+open import Function.Bundles using (_↔_; _↣_; Injection; _⇔_; mk⇔)
 open import Function.Related.TypeIsomorphisms using (×-comm; ∃∃↔∃∃)
 open import Function.Construct.Identity using (↔-id)
 open import Level using (Level)
@@ -55,6 +55,9 @@ private
   variable
     ℓ : Level
     A B C : Set ℓ
+    x y v : A
+    xs ys : List A
+    xss : List (List A)
 
 ------------------------------------------------------------------------
 -- Publicly re-export properties from Core
@@ -64,10 +67,10 @@ open import Data.List.Membership.Propositional.Properties.Core public
 ------------------------------------------------------------------------
 -- Equality
 
-∈-resp-≋ : ∀ {x : A} → (x ∈_) Respects _≋_
+∈-resp-≋ : (x ∈_) Respects _≋_
 ∈-resp-≋ = Membership.∈-resp-≋ (≡.setoid _)
 
-∉-resp-≋ : ∀ {x : A} → (x ∉_) Respects _≋_
+∉-resp-≋ : (x ∉_) Respects _≋_
 ∉-resp-≋ = Membership.∉-resp-≋ (≡.setoid _)
 
 ------------------------------------------------------------------------
@@ -96,14 +99,14 @@ map-mapWith∈ = Membership.map-mapWith∈ (≡.setoid _)
 
 module _ (f : A → B) where
 
-  ∈-map⁺ : ∀ {x xs} → x ∈ xs → f x ∈ map f xs
+  ∈-map⁺ : x ∈ xs → f x ∈ map f xs
   ∈-map⁺ = Membership.∈-map⁺ (≡.setoid A) (≡.setoid B) (cong f)
 
-  ∈-map⁻ : ∀ {y xs} → y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x
+  ∈-map⁻ : y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x
   ∈-map⁻ = Membership.∈-map⁻ (≡.setoid A) (≡.setoid B)
 
-  map-∈↔ : ∀ {y xs} → (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs
-  map-∈↔ {y} {xs} =
+  map-∈↔ : (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs
+  map-∈↔ {xs} {y} =
     (∃ λ x → x ∈ xs × y ≡ f x)   ↔⟨ Any↔ ⟩
     Any (λ x → y ≡ f x) xs       ↔⟨ map↔ ⟩
     y ∈ List.map f xs            ∎
@@ -114,7 +117,7 @@ module _ (f : A → B) where
 
 module _ {v : A} where
 
-  ∈-++⁺ˡ : ∀ {xs ys} → v ∈ xs → v ∈ xs ++ ys
+  ∈-++⁺ˡ : v ∈ xs → v ∈ xs ++ ys
   ∈-++⁺ˡ = Membership.∈-++⁺ˡ (≡.setoid A)
 
   ∈-++⁺ʳ : ∀ xs {ys} → v ∈ ys → v ∈ xs ++ ys
@@ -123,10 +126,13 @@ module _ {v : A} where
   ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
   ∈-++⁻ = Membership.∈-++⁻ (≡.setoid A)
 
+  ++-∈⇔ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
+  ++-∈⇔ = mk⇔ (∈-++⁻ _) Sum.[ ∈-++⁺ˡ , ∈-++⁺ʳ _ ]
+
   ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys
   ∈-insert xs = Membership.∈-insert (≡.setoid A) xs refl
 
-  ∈-∃++ : ∀ {xs} → v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs
+  ∈-∃++ : v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs
   ∈-∃++ v∈xs
     with ys , zs , _ , refl , eq ← Membership.∈-∃++ (≡.setoid A) v∈xs
     = ys , zs , ≋⇒≡ eq
@@ -136,7 +142,7 @@ module _ {v : A} where
 
 module _ {v : A} where
 
-  ∈-concat⁺ : ∀ {xss} → Any (v ∈_) xss → v ∈ concat xss
+  ∈-concat⁺ : Any (v ∈_) xss → v ∈ concat xss
   ∈-concat⁺ = Membership.∈-concat⁺ (≡.setoid A)
 
   ∈-concat⁻ : ∀ xss → v ∈ concat xss → Any (v ∈_) xss
@@ -151,8 +157,7 @@ module _ {v : A} where
     let xs , v∈xs , xs∈xss = Membership.∈-concat⁻′ (≡.setoid A) xss v∈c
     in xs , v∈xs , Any.map ≋⇒≡ xs∈xss
 
-  concat-∈↔ : ∀ {xss : List (List A)} →
-              (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss
+  concat-∈↔ : (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss
   concat-∈↔ {xss} =
     (∃ λ xs → v ∈ xs × xs ∈ xss)  ↔⟨ Σ.cong (↔-id _) $ ×-comm _ _ ⟩
     (∃ λ xs → xs ∈ xss × v ∈ xs)  ↔⟨ Any↔ ⟩
@@ -160,6 +165,19 @@ module _ {v : A} where
     v ∈ concat xss                ∎
     where open Related.EquationalReasoning
 
+------------------------------------------------------------------------
+-- concatMap
+
+module _ (f : A → List B) {xs y} where
+
+  private Sᴬ = ≡.setoid A; Sᴮ = ≡.setoid B
+
+  ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁺ = Membership.∈-concatMap⁺ Sᴬ Sᴮ
+
+  ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∈-concatMap⁻ = Membership.∈-concatMap⁻ Sᴬ Sᴮ
+
 ------------------------------------------------------------------------
 -- cartesianProductWith
 
@@ -246,12 +264,25 @@ module _ {n} {f : Fin n → A} where
 
 module _ {p} {P : A → Set p} (P? : Decidable P) where
 
-  ∈-filter⁺ : ∀ {x xs} → x ∈ xs → P x → x ∈ filter P? xs
+  ∈-filter⁺ : x ∈ xs → P x → x ∈ filter P? xs
   ∈-filter⁺ = Membership.∈-filter⁺ (≡.setoid A) P? (≡.resp P)
 
-  ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
+  ∈-filter⁻ : v ∈ filter P? xs → v ∈ xs × P v
   ∈-filter⁻ = Membership.∈-filter⁻ (≡.setoid A) P? (≡.resp P)
 
+------------------------------------------------------------------------
+-- map∘filter
+
+module _ (f : A → B) {p} {P : A → Set p} (P? : Decidable P) {f xs y} where
+
+  private Sᴬ = ≡.setoid A; Sᴮ = ≡.setoid B; respP = ≡.resp P
+
+  ∈-map∘filter⁻ : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x)
+  ∈-map∘filter⁻ = Membership.∈-map∘filter⁻ Sᴬ Sᴮ P? respP
+
+  ∈-map∘filter⁺ : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs)
+  ∈-map∘filter⁺ = Membership.∈-map∘filter⁺ Sᴬ Sᴮ P? respP (cong f)
+
 ------------------------------------------------------------------------
 -- derun and deduplicate
 
@@ -268,8 +299,13 @@ module _ (_≈?_ : DecidableEquality A) where
   ∈-derun⁺ : ∀ {xs z} → z ∈ xs → z ∈ derun _≈?_ xs
   ∈-derun⁺ z∈xs = Membership.∈-derun⁺ (≡.setoid A) _≈?_ (flip trans) z∈xs
 
+  private resp≈ = λ {c b a : A} (c≡b : c ≡ b) (a≡b : a ≡ b) → trans a≡b (sym c≡b)
+
   ∈-deduplicate⁺ : ∀ {xs z} → z ∈ xs → z ∈ deduplicate _≈?_ xs
-  ∈-deduplicate⁺ z∈xs = Membership.∈-deduplicate⁺ (≡.setoid A) _≈?_ (λ c≡b a≡b → trans a≡b (sym c≡b)) z∈xs
+  ∈-deduplicate⁺ z∈xs = Membership.∈-deduplicate⁺ (≡.setoid A) _≈?_ resp≈ z∈xs
+
+  deduplicate-∈⇔ : ∀ {xs z} → z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
+  deduplicate-∈⇔ = Membership.deduplicate-∈⇔ (≡.setoid A) _≈?_ resp≈
 
 ------------------------------------------------------------------------
 -- _>>=_
@@ -310,13 +346,13 @@ module _ (_≈?_ : DecidableEquality A) where
 ------------------------------------------------------------------------
 -- length
 
-∈-length : ∀ {x : A} {xs} → x ∈ xs → 0 < length xs
+∈-length : x ∈ xs → 0 < length xs
 ∈-length = Membership.∈-length (≡.setoid _)
 
 ------------------------------------------------------------------------
 -- lookup
 
-∈-lookup : ∀ {xs : List A} i → lookup xs i ∈ xs
+∈-lookup : ∀ i → lookup xs i ∈ xs
 ∈-lookup {xs = xs} i = Membership.∈-lookup (≡.setoid _) xs i
 
 ------------------------------------------------------------------------
@@ -337,7 +373,7 @@ module _ {_•_ : Op₂ A} where
 ------------------------------------------------------------------------
 -- inits
 
-[]∈inits : ∀ {a} {A : Set a} (as : List A) → [] ∈ inits as
+[]∈inits : (as : List A) → [] ∈ inits as
 []∈inits _ = here refl
 
 ------------------------------------------------------------------------
@@ -401,3 +437,39 @@ there-injective-≢∈ : ∀ {xs} {x y z : A} {x∈xs : x ∈ xs} {y∈xs : y 
                      there {x = z} x∈xs ≢∈ there y∈xs →
                      x∈xs ≢∈ y∈xs
 there-injective-≢∈ neq refl eq = neq refl (≡.cong there eq)
+
+------------------------------------------------------------------------
+-- AllPairs
+
+open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
+import Data.List.Relation.Unary.All as All
+
+module _ {R : A → A → Set ℓ} where
+  ∈-AllPairs₂ : ∀ {xs x y} → AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
+  ∈-AllPairs₂ (_ ∷ _)  (here refl) (here refl) = inj₁ refl
+  ∈-AllPairs₂ (p ∷ _)  (here refl) (there y∈)  = inj₂ $ inj₁ $ All.lookup p y∈
+  ∈-AllPairs₂ (p ∷ _)  (there x∈)  (here refl) = inj₂ $ inj₂ $ All.lookup p x∈
+  ∈-AllPairs₂ (_ ∷ ps) (there x∈)  (there y∈)  = ∈-AllPairs₂ ps x∈ y∈
+
+------------------------------------------------------------------------
+-- nested lists
+
+[]∉map∷ : (List A ∋ []) ∉ map (x ∷_) xss
+[]∉map∷ {xss = _ ∷ _} (there p) = []∉map∷ p
+
+map∷-decomp∈ : (List A ∋ x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
+map∷-decomp∈ {xss = _ ∷ _} = λ where
+  (here refl) → refl , here refl
+  (there p)   → map₂ there $ map∷-decomp∈ p
+
+map∷-decomp : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs
+map∷-decomp               {xss = _  ∷ _} (here refl) = -, here refl , refl
+map∷-decomp {xs = []}     {xss = _  ∷ _} (there xs∈) = contradiction xs∈ []∉map∷
+map∷-decomp {xs = x ∷ xs} {xss = _  ∷ _} (there xs∈) =
+  let eq , p = map∷-decomp∈ xs∈
+  in -, there p , cong (_∷ _) (sym eq)
+
+∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs
+∈-map∷⁻ {xss = _ ∷ _} = λ where
+  (here refl) → here refl
+  (there p)   → ∈-map∷⁻ p
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index 5c77e40b96..65485abb0e 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -12,7 +12,7 @@
 
 module Data.List.Membership.Propositional.Properties.Core where
 
-open import Data.List.Base using (List)
+open import Data.List.Base using (List; [])
 open import Data.List.Membership.Propositional
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product.Base as Product using (_,_; ∃; _×_)
@@ -30,6 +30,12 @@ private
     x : A
     xs : List A
 
+------------------------------------------------------------------------
+-- Basics
+
+∉[] : x ∉ []
+∉[] ()
+
 ------------------------------------------------------------------------
 -- find satisfies a simple equality when the predicate is a
 -- propositional equality.
diff --git a/src/Data/List/Membership/Propositional/Properties/WithK.agda b/src/Data/List/Membership/Propositional/Properties/WithK.agda
index a86f23a8ea..656ec11dae 100644
--- a/src/Data/List/Membership/Propositional/Properties/WithK.agda
+++ b/src/Data/List/Membership/Propositional/Properties/WithK.agda
@@ -9,17 +9,31 @@
 
 module Data.List.Membership.Propositional.Properties.WithK where
 
+open import Level using (Level)
+open import Function.Bundles using (Equivalence)
 open import Data.List.Base
 open import Data.List.Relation.Unary.Unique.Propositional
 open import Data.List.Membership.Propositional
 import Data.List.Membership.Setoid.Properties as Membership
+open import Data.List.Relation.Binary.BagAndSetEquality using (_∼[_]_; set; bag)
+open import Data.Product using (_,_)
 open import Relation.Unary using (Irrelevant)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Relation.Binary.PropositionalEquality.WithK
+open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)
+
+private
+  variable
+    a : Level
+    A : Set a
+    xs ys : List A
 
 ------------------------------------------------------------------------
 -- Irrelevance
 
-unique⇒irrelevant : ∀ {a} {A : Set a} {xs : List A} →
-                    Unique xs → Irrelevant (_∈ xs)
+unique⇒irrelevant : Unique xs → Irrelevant (_∈ xs)
 unique⇒irrelevant = Membership.unique⇒irrelevant (≡.setoid _) ≡-irrelevant
+
+unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
+unique∧set⇒bag p p′ eq = record
+  { Equivalence eq
+  ; inverse = (λ _ → unique⇒irrelevant p′ _ _) , (λ _ → unique⇒irrelevant p _ _) }
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 76bbd8beaf..988c01a07e 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -1,4 +1,4 @@
-------------------------------------------------------------------------
+-----------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to setoid list membership
@@ -21,11 +21,11 @@ import Data.List.Relation.Unary.All.Properties.Core as All
 import Data.List.Relation.Unary.Any.Properties as Any
 import Data.List.Relation.Unary.Unique.Setoid as Unique
 open import Data.Nat.Base using (suc; z<s; _<_)
-open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂)
+open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂; ∃-syntax)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_$_; flip; _∘_; _∘′_; id)
-open import Function.Bundles using (_↔_)
+open import Function.Bundles using (_↔_; mk↔; _⇔_; mk⇔)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_; _Preserves_⟶_)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
@@ -42,6 +42,16 @@ private
   variable
     c c₁ c₂ c₃ p ℓ ℓ₁ ℓ₂ ℓ₃ : Level
 
+------------------------------------------------------------------------
+-- Basics
+
+module _ (S : Setoid c ℓ) where
+
+  open Membership S
+
+  ∉[] : ∀ {x} → x ∉ []
+  ∉[] ()
+
 ------------------------------------------------------------------------
 -- Equality properties
 
@@ -65,6 +75,14 @@ module _ (S : Setoid c ℓ) where
   ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_
   ∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys)
 
+  -- x ∉_ is equivalent to All (x ≉_)
+
+  ∉⇒All[≉] : ∀ {x xs} → x ∉ xs → All (x ≉_) xs
+  ∉⇒All[≉] = All.¬Any⇒All¬ _
+
+  All[≉]⇒∉ : ∀ {x xs} → All (x ≉_) xs → x ∉ xs
+  All[≉]⇒∉ = All.All¬⇒¬Any
+
   -- index is injective in its first argument.
 
   index-injective : ∀ {x₁ x₂ xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) →
@@ -83,7 +101,7 @@ module _ (S : Setoid c ℓ) where
 
   private
     ∉×∈⇒≉ : ∀ {x y xs} → All (y ≉_) xs → x ∈ xs → x ≉ y
-    ∉×∈⇒≉ = All.lookupWith λ y≉z x≈z x≈y → y≉z (trans (sym x≈y) x≈z)
+    ∉×∈⇒≉ ≉s x∈xs x≈y = All[≉]⇒∉ S ≉s (∈-resp-≈ S x≈y x∈xs)
 
   unique⇒irrelevant : Binary.Irrelevant _≈_ → ∀ {xs} → Unique xs → Unary.Irrelevant (_∈ xs)
   unique⇒irrelevant ≈-irr _        (here p)  (here q)  =
@@ -239,6 +257,21 @@ module _ (S : Setoid c ℓ) where
   ∈-concat⁻′ xss v∈c[xss] =
     let xs , xs∈xss , v∈xs = find (∈-concat⁻ xss v∈c[xss]) in xs , v∈xs , xs∈xss
 
+------------------------------------------------------------------------
+-- concatMap
+
+module _
+  (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂)
+  {f : Carrier S₁ → List (Carrier S₂)} {xs y} where
+
+  open Membership S₂ using (_∈_)
+
+  ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
+  ∈-concatMap⁺ = Any.concatMap⁺ f
+
+  ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∈-concatMap⁻ = Any.concatMap⁻ f
+
 ------------------------------------------------------------------------
 -- reverse
 
@@ -363,6 +396,33 @@ module _ (S : Setoid c ℓ) {P : Pred (Carrier S) p}
   ...   | here  v≈x   = here v≈x , resp (sym v≈x) (invert [Px])
   ...   | there v∈fxs = Product.map there id (∈-filter⁻ v∈fxs)
 
+------------------------------------------------------------------------
+-- map∘filter
+
+module _
+  (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂)
+  {P : Pred _ p} (P? : Decidable P) (resp : P Respects _)
+  {f xs y} where
+
+  open Setoid     S₁ renaming (_≈_ to _≈₁_)
+  open Setoid     S₂ renaming (_≈_ to _≈₂_; sym to sym₂)
+  open Membership S₁ renaming (_∈_ to _∈₁_)
+  open Membership S₂ renaming (_∈_ to _∈₂_)
+
+  ∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) →
+                  ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
+  ∈-map∘filter⁻ h =
+    let x , x∈ , y≈ = ∈-map⁻ S₁ S₂ h
+        y∈ , Py     = ∈-filter⁻ S₁ P? resp x∈
+    in x , y∈ , y≈ , Py
+
+  ∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ →
+                  ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
+                  y ∈₂ map f (filter P? xs)
+  ∈-map∘filter⁺ pres (x , x∈ , y≈ , Px)
+    = ∈-resp-≈ S₂ (sym₂ y≈)
+    $ ∈-map⁺ S₁ S₂ pres (∈-filter⁺ S₁ P? resp x∈ Px)
+
 ------------------------------------------------------------------------
 -- derun and deduplicate
 
@@ -374,16 +434,20 @@ module _ (S : Setoid c ℓ) {R : Rel (Carrier S) ℓ₂} (R? : Binary.Decidable
   ∈-derun⁺ : _≈_ Respectsʳ R → ∀ {xs z} → z ∈ xs → z ∈ derun R? xs
   ∈-derun⁺ ≈-resp-R z∈xs = Any.derun⁺ R? ≈-resp-R z∈xs
 
+  ∈-derun⁻ : ∀ xs {z} → z ∈ derun R? xs → z ∈ xs
+  ∈-derun⁻ xs z∈derun[R,xs] = Any.derun⁻ R? z∈derun[R,xs]
+
   ∈-deduplicate⁺ : _≈_ Respectsʳ (flip R) → ∀ {xs z} →
                    z ∈ xs → z ∈ deduplicate R? xs
   ∈-deduplicate⁺ ≈-resp-R z∈xs = Any.deduplicate⁺ R? ≈-resp-R z∈xs
 
-  ∈-derun⁻ : ∀ xs {z} → z ∈ derun R? xs → z ∈ xs
-  ∈-derun⁻ xs z∈derun[R,xs] = Any.derun⁻ R? z∈derun[R,xs]
-
   ∈-deduplicate⁻ : ∀ xs {z} → z ∈ deduplicate R? xs → z ∈ xs
   ∈-deduplicate⁻ xs z∈dedup[R,xs] = Any.deduplicate⁻ R? z∈dedup[R,xs]
 
+  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → ∀ {xs z} →
+                   z ∈ xs ⇔ z ∈ deduplicate R? xs
+  deduplicate-∈⇔ p = mk⇔ (∈-deduplicate⁺ p) (∈-deduplicate⁻ _)
+
 ------------------------------------------------------------------------
 -- length
 
@@ -461,4 +525,3 @@ module _ (S : Setoid c ℓ) where
 
   All-∉-swap :  ∀ {xs ys} → All (_∉ ys) xs → All (_∉ xs) ys
   All-∉-swap p = All.¬Any⇒All¬ _ ((All.All¬⇒¬Any p) ∘ Any-∈-swap)
-
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index f847d8a059..71d7b90b7f 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -715,6 +715,14 @@ map-concatMap f g xs = begin
   concatMap (map f ∘′ g) xs
     ∎
 
+concatMap-++ : ∀ (f : A → List B) xs ys →
+               concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
+concatMap-++ f xs ys = begin
+  concatMap f (xs ++ ys)           ≡⟨⟩
+  concat (map f (xs ++ ys))        ≡⟨ cong concat $ map-++ f xs ys ⟩
+  concat (map f xs ++ map f ys)    ≡˘⟨ concat-++ (map f xs) (map f ys) ⟩
+  concatMap f xs ++ concatMap f ys ∎ where open ≡-Reasoning
+
 ------------------------------------------------------------------------
 -- catMaybes
 
diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 815b27db89..b27e45d585 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -27,9 +27,9 @@ open import Data.List.Membership.Propositional.Properties
 open import Data.List.Relation.Binary.Subset.Propositional.Properties
   using (⊆-preorder)
 open import Data.List.Relation.Binary.Permutation.Propositional
-  using (_↭_; ↭-sym; refl; module PermutationReasoning)
+  using (_↭_; ↭-refl; ↭-sym; ↭-prep; module PermutationReasoning)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties
-  using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ↭-sym-involutive; shift; ++-comm)
+  using (∈-resp-↭; ∈-resp-[σ⁻¹∘σ]; ∈-resp-[σ∘σ⁻¹]; shift; ++-comm)
 open import Data.Product.Base as Product using (∃; _,_; proj₁; proj₂; _×_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂)
@@ -574,29 +574,18 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys =
 
 
 ------------------------------------------------------------------------
--- Relationships to other relations
+-- Relationships to propositional permutation
 
 ↭⇒∼bag : _↭_ {A = A} ⇒ _∼[ bag ]_
-↭⇒∼bag xs↭ys {v} = mk↔ₛ′ (to xs↭ys) (from xs↭ys) (to∘from xs↭ys) (from∘to xs↭ys)
-  where
-  to : ∀ {xs ys} → xs ↭ ys → v ∈ xs → v ∈ ys
-  to xs↭ys = ∈-resp-↭ xs↭ys
-
-  from : ∀ {xs ys} → xs ↭ ys → v ∈ ys → v ∈ xs
-  from xs↭ys = ∈-resp-↭ (↭-sym xs↭ys)
-
-  from∘to : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ xs) → from p (to p q) ≡ q
-  from∘to = ∈-resp-[σ⁻¹∘σ]
-
-  to∘from : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ ys) → to p (from p q) ≡ q
-  to∘from p with res ← from∘to (↭-sym p) rewrite ↭-sym-involutive p = res
+↭⇒∼bag xs↭ys {v} =
+  mk↔ₛ′ (∈-resp-↭ xs↭ys) (∈-resp-↭ (↭-sym xs↭ys)) (∈-resp-[σ∘σ⁻¹] xs↭ys) (∈-resp-[σ⁻¹∘σ] xs↭ys)
 
 ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A}
-∼bag⇒↭ {A = A} {[]} eq with refl ← empty-unique (↔-sym eq) = refl
+∼bag⇒↭ {A = A} {[]}     eq with refl ← empty-unique (↔-sym eq) = ↭-refl
 ∼bag⇒↭ {A = A} {x ∷ xs} eq
-  with zs₁ , zs₂ , p ← ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) rewrite p = begin
-    x ∷ xs           <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩
-    x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩
+  with zs₁ , zs₂ , refl ← ∈-∃++ (Inverse.to (eq {x}) (here refl)) = begin
+    x ∷ xs           ↭⟨ ↭-prep x (∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂))))) ⟩
+    x ∷ (zs₂ ++ zs₁) ↭⟨ ↭-prep x (++-comm zs₂ zs₁) ⟩
     x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨
     zs₁ ++ x ∷ zs₂   ∎
     where
diff --git a/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
new file mode 100644
index 0000000000..b2b2ec591c
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
@@ -0,0 +1,65 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of disjoint lists (propositional equality)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Binary.Disjoint.Propositional.Properties where
+
+open import Level using (Level)
+open import Function.Base using (_∘_)
+open import Function.Bundles using (_⇔_)
+open import Data.List.Base
+open import Data.List.Relation.Binary.Disjoint.Propositional
+import Data.List.Relation.Unary.Any as Any
+open import Data.List.Relation.Unary.All as All
+open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
+open import Data.List.Relation.Unary.Any.Properties using (++⁻)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.Product.Base as Product using (_,_)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Symmetric; DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Relation.Nullary.Negation using (¬_)
+
+import Data.List.Relation.Binary.Disjoint.Setoid.Properties as S
+
+module _ {a} {A : Set a} where
+
+  private
+    Sᴬ = setoid A
+    variable
+      x : A
+      xs ys vs : List A
+      xss : List (List A)
+
+  ------------------------------------------------------------------------
+  -- Relational properties
+  ------------------------------------------------------------------------
+
+  sym : Symmetric Disjoint
+  sym = S.sym Sᴬ
+
+  ------------------------------------------------------------------------
+  -- Relationship with other predicates
+  ------------------------------------------------------------------------
+
+  Disjoint⇒AllAll : Disjoint xs ys → All (λ x → All (λ y → ¬ x ≡ y) ys) xs
+  Disjoint⇒AllAll = S.Disjoint⇒AllAll Sᴬ
+
+  ------------------------------------------------------------------------
+  -- Introduction (⁺) and elimination (⁻) rules for list operations
+  ------------------------------------------------------------------------
+  -- concat
+
+  concat⁺ʳ : All (Disjoint vs) xss → Disjoint vs (concat xss)
+  concat⁺ʳ = S.concat⁺ʳ (setoid _)
+
+  -- deduplicate
+  module _ (_≟_ : DecidableEquality A) where
+    deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+    deduplicate⁺ = S.deduplicate⁺ Sᴬ _≟_
diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
index bc5a95fc77..3416fc31e8 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
@@ -8,49 +8,57 @@
 
 module Data.List.Relation.Binary.Disjoint.Setoid.Properties where
 
+open import Function.Base using (_∘_)
+open import Function.Bundles using (_⇔_; mk⇔)
 open import Data.List.Base
 open import Data.List.Relation.Binary.Disjoint.Setoid
 import Data.List.Relation.Unary.Any as Any
 open import Data.List.Relation.Unary.All as All
 open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
 open import Data.List.Relation.Unary.Any.Properties using (++⁻)
-open import Data.Product.Base using (_,_)
+import Data.List.Membership.Setoid.Properties as Mem
+open import Data.Product.Base as Product using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions using (Symmetric)
+open import Relation.Binary.Definitions using (Symmetric; DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Nullary.Negation using (¬_)
 
-------------------------------------------------------------------------
--- Relational properties
-------------------------------------------------------------------------
-
 module _ {c ℓ} (S : Setoid c ℓ) where
 
-  sym : Symmetric (Disjoint S)
-  sym xs#ys (v∈ys , v∈xs) = xs#ys (v∈xs , v∈ys)
+  open Setoid S using (_≉_; reflexive) renaming (Carrier to A)
 
-------------------------------------------------------------------------
--- Relationship with other predicates
-------------------------------------------------------------------------
+  ------------------------------------------------------------------------
+  -- Relational properties
+  ------------------------------------------------------------------------
 
-module _ {c ℓ} (S : Setoid c ℓ) where
+  sym : Symmetric (Disjoint S)
+  sym xs#ys (v∈ys , v∈xs) = xs#ys (v∈xs , v∈ys)
 
-  open Setoid S
+  ------------------------------------------------------------------------
+  -- Relationship with other predicates
+  ------------------------------------------------------------------------
 
   Disjoint⇒AllAll : ∀ {xs ys} → Disjoint S xs ys →
-                    All (λ x → All (λ y → ¬ x ≈ y) ys) xs
+                    All (λ x → All (x ≉_) ys) xs
   Disjoint⇒AllAll xs#ys = All.map (¬Any⇒All¬ _)
     (All.tabulate (λ v∈xs v∈ys → xs#ys (Any.map reflexive v∈xs , v∈ys)))
 
-------------------------------------------------------------------------
--- Introduction (⁺) and elimination (⁻) rules for list operations
-------------------------------------------------------------------------
--- concat
-
-module _ {c ℓ} (S : Setoid c ℓ) where
+  ------------------------------------------------------------------------
+  -- Introduction (⁺) and elimination (⁻) rules for list operations
+  ------------------------------------------------------------------------
+  -- concat
 
   concat⁺ʳ : ∀ {vs xss} → All (Disjoint S vs) xss → Disjoint S vs (concat xss)
   concat⁺ʳ {xss = xs ∷ xss} (vs#xs ∷ vs#xss) (v∈vs , v∈xs++concatxss)
     with ++⁻ xs v∈xs++concatxss
   ... | inj₁ v∈xs  = vs#xs (v∈vs , v∈xs)
   ... | inj₂ v∈xss = concat⁺ʳ vs#xss (v∈vs , v∈xss)
+
+  -- deduplicate
+  module _ (_≟_ : DecidableEquality A) where
+
+    deduplicate⁺ : ∀ {xs ys} → Disjoint S xs ys →
+                   Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
+    deduplicate⁺ = let ∈-dedup⁻ = Mem.∈-deduplicate⁻ S _≟_ in
+      _∘ Product.map (∈-dedup⁻ _) (∈-dedup⁻ _)
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
index 12015b3076..686c569423 100644
--- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
@@ -11,8 +11,8 @@ module Data.List.Relation.Binary.Permutation.Homogeneous where
 open import Data.List.Base using (List; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
   using (Pointwise)
-open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise
-  using (symmetric)
+import Data.List.Relation.Binary.Pointwise.Properties as Pointwise
+open import Data.Nat.Base using (ℕ; suc; _+_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
@@ -59,3 +59,11 @@ map R⇒S (refl xs∼ys)         = refl (Pointwise.map R⇒S xs∼ys)
 map R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map R⇒S xs∼ys)
 map R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys)
 map R⇒S (trans xs∼ys ys∼zs)  = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)
+
+-- Measures the number of constructors, can be useful for termination proofs
+
+steps : ∀ {R : Rel A r} {xs ys} → Permutation R xs ys → ℕ
+steps (refl _)            = 1
+steps (prep _ xs↭ys)      = suc (steps xs↭ys)
+steps (swap _ _ xs↭ys)    = suc (steps xs↭ys)
+steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index c41793d28a..0e13a5e3ba 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -10,14 +10,22 @@ module Data.List.Relation.Binary.Permutation.Propositional
   {a} {A : Set a} where
 
 open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Relation.Binary.Equality.Propositional using (_≋_; ≋⇒≡)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.Definitions using (Reflexive; Transitive)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 open import Relation.Binary.Reasoning.Syntax
 
+import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+
+private
+  variable
+    x y z v w : A
+    ws xs ys zs : List A
+
 ------------------------------------------------------------------------
 -- An inductive definition of permutation
 
@@ -30,21 +38,32 @@ open import Relation.Binary.Reasoning.Syntax
 infix 3 _↭_
 
 data _↭_ : Rel (List A) a where
-  refl  : ∀ {xs}        → xs ↭ xs
-  prep  : ∀ {xs ys} x   → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-  swap  : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
-  trans : ∀ {xs ys zs}  → xs ↭ ys → ys ↭ zs → xs ↭ zs
+  refl  : xs ↭ xs
+  prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
+  swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
+  trans : xs ↭ ys → ys ↭ zs → xs ↭ zs
+
+-- Constructor aliases
+
+↭-refl : Reflexive _↭_
+↭-refl = refl
+
+↭-prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
+↭-prep = prep
+
+↭-swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
+↭-swap = swap
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl
+↭-reflexive refl = ↭-refl
 
-↭-refl : Reflexive _↭_
-↭-refl = refl
+↭-reflexive-≋ : _≋_ ⇒ _↭_
+↭-reflexive-≋ xs≋ys = ↭-reflexive (≋⇒≡ xs≋ys)
 
-↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs
+↭-sym : xs ↭ ys → ys ↭ xs
 ↭-sym refl                = refl
 ↭-sym (prep x xs↭ys)      = prep x (↭-sym xs↭ys)
 ↭-sym (swap x y xs↭ys)    = swap y x (↭-sym xs↭ys)
@@ -58,7 +77,7 @@ data _↭_ : Rel (List A) a where
 
 ↭-isEquivalence : IsEquivalence _↭_
 ↭-isEquivalence = record
-  { refl  = refl
+  { refl  = ↭-refl
   ; sym   = ↭-sym
   ; trans = ↭-trans
   }
@@ -68,6 +87,28 @@ data _↭_ : Rel (List A) a where
   { isEquivalence = ↭-isEquivalence
   }
 
+------------------------------------------------------------------------
+-- _↭_ is equivalent to `Setoid`-based permutation
+
+private
+  open module ↭ₛ = Permutation (≡.setoid A)
+    using ()
+    renaming (_↭_ to _↭ₛ_)
+
+↭⇒↭ₛ : xs ↭ ys → xs ↭ₛ ys
+↭⇒↭ₛ refl         = ↭ₛ.↭-refl
+↭⇒↭ₛ (prep x p)   = ↭ₛ.↭-prep x (↭⇒↭ₛ p)
+↭⇒↭ₛ (swap x y p) = ↭ₛ.↭-swap x y (↭⇒↭ₛ p)
+↭⇒↭ₛ (trans p q)  = ↭ₛ.↭-trans′ (↭⇒↭ₛ p) (↭⇒↭ₛ q)
+
+
+↭ₛ⇒↭ : _↭ₛ_ ⇒ _↭_
+↭ₛ⇒↭ (↭ₛ.refl xs≋ys)       = ↭-reflexive-≋ xs≋ys
+↭ₛ⇒↭ (↭ₛ.prep refl p)      = ↭-prep _ (↭ₛ⇒↭ p)
+↭ₛ⇒↭ (↭ₛ.swap refl refl p) = ↭-swap _ _ (↭ₛ⇒↭ p)
+↭ₛ⇒↭ (↭ₛ.trans p q)        = ↭-trans (↭ₛ⇒↭ p) (↭ₛ⇒↭ q)
+
+
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs and allow "zooming in"
 -- to localised reasoning.
@@ -89,12 +130,12 @@ module PermutationReasoning where
   -- Skip reasoning on the first element
   step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
               xs ↭ ys → (x ∷ xs) IsRelatedTo zs
-  step-prep x xs rel xs↭ys = relTo (trans (prep x xs↭ys) (begin rel))
+  step-prep x xs rel xs↭ys = ↭-go (↭-prep x xs↭ys) rel
 
   -- Skip reasoning about the first two elements
   step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
               xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
-  step-swap x y xs rel xs↭ys = relTo (trans (swap x y xs↭ys) (begin rel))
+  step-swap x y xs rel xs↭ys = ↭-go (↭-swap x y xs↭ys) rel
 
   syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
   syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index 6fe439ed03..30cd2bdcc0 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -12,16 +12,16 @@ open import Algebra.Bundles
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Nat.Base using (suc; _*_)
-open import Data.Nat.Properties using (*-assoc; *-comm)
-open import Data.Product.Base using (-,_; proj₂)
+open import Data.Nat.Base using (ℕ; suc)
+import Data.Nat.Properties as ℕ
+open import Data.Product.Base using (-,_)
 open import Data.List.Base as List
 open import Data.List.Relation.Binary.Permutation.Propositional
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
-import Data.List.Properties as Lₚ
+import Data.List.Properties as List
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Base using (_∘_; _⟨_⟩_; _$_)
@@ -34,6 +34,8 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
 open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
 open import Relation.Nullary
 
+import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutation
+
 private
   variable
     a b p : Level
@@ -70,49 +72,58 @@ private
 ------------------------------------------------------------------------
 -- Relationships to other predicates
 
-All-resp-↭ : ∀ {P : Pred A p} → (All P) Respects _↭_
-All-resp-↭ refl wit                     = wit
-All-resp-↭ (prep x p) (px ∷ wit)        = px ∷ All-resp-↭ p wit
-All-resp-↭ (swap x y p) (px ∷ py ∷ wit) = py ∷ px ∷ All-resp-↭ p wit
-All-resp-↭ (trans p₁ p₂) wit            = All-resp-↭ p₂ (All-resp-↭ p₁ wit)
-
-Any-resp-↭ : ∀ {P : Pred A p} → (Any P) Respects _↭_
-Any-resp-↭ refl         wit                 = wit
-Any-resp-↭ (prep x p)   (here px)           = here px
-Any-resp-↭ (prep x p)   (there wit)         = there (Any-resp-↭ p wit)
-Any-resp-↭ (swap x y p) (here px)           = there (here px)
-Any-resp-↭ (swap x y p) (there (here px))   = here px
-Any-resp-↭ (swap x y p) (there (there wit)) = there (there (Any-resp-↭ p wit))
-Any-resp-↭ (trans p p₁) wit                 = Any-resp-↭ p₁ (Any-resp-↭ p wit)
+module _ {P : Pred A p} where
+
+  All-resp-↭ : (All P) Respects _↭_
+  All-resp-↭ refl wit                     = wit
+  All-resp-↭ (prep x p) (px ∷ wit)        = px ∷ All-resp-↭ p wit
+  All-resp-↭ (swap x y p) (px ∷ py ∷ wit) = py ∷ px ∷ All-resp-↭ p wit
+  All-resp-↭ (trans p₁ p₂) wit            = All-resp-↭ p₂ (All-resp-↭ p₁ wit)
+
+  Any-resp-↭ : (Any P) Respects _↭_
+  Any-resp-↭ refl         wit                 = wit
+  Any-resp-↭ (prep x p)   (here px)           = here px
+  Any-resp-↭ (prep x p)   (there wit)         = there (Any-resp-↭ p wit)
+  Any-resp-↭ (swap x y p) (here px)           = there (here px)
+  Any-resp-↭ (swap x y p) (there (here px))   = here px
+  Any-resp-↭ (swap x y p) (there (there wit)) = there (there (Any-resp-↭ p wit))
+  Any-resp-↭ (trans p p₁) wit                 = Any-resp-↭ p₁ (Any-resp-↭ p wit)
+
+  Any-resp-[σ⁻¹∘σ] : ∀ {xs ys} (σ : xs ↭ ys) (ix : Any P xs) →
+                     Any-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix
+  Any-resp-[σ⁻¹∘σ] refl          ix               = refl
+  Any-resp-[σ⁻¹∘σ] (prep _ _)    (here _)         = refl
+  Any-resp-[σ⁻¹∘σ] (swap _ _ _)  (here _)         = refl
+  Any-resp-[σ⁻¹∘σ] (swap _ _ _)  (there (here _)) = refl
+  Any-resp-[σ⁻¹∘σ] (trans σ₁ σ₂) ix
+    rewrite Any-resp-[σ⁻¹∘σ] σ₂ (Any-resp-↭ σ₁ ix)
+    rewrite Any-resp-[σ⁻¹∘σ] σ₁ ix
+    = refl
+  Any-resp-[σ⁻¹∘σ] (prep _ σ)    (there ix)
+    rewrite Any-resp-[σ⁻¹∘σ] σ ix
+    = refl
+  Any-resp-[σ⁻¹∘σ] (swap _ _ σ)  (there (there ix))
+    rewrite Any-resp-[σ⁻¹∘σ] σ ix
+    = refl
+
+  Any-resp-[σ∘σ⁻¹] : ∀ {xs ys} (σ : xs ↭ ys) (iy : Any P ys) →
+                     Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
+  Any-resp-[σ∘σ⁻¹] p
+    with res ← Any-resp-[σ⁻¹∘σ] (↭-sym p)
+    rewrite ↭-sym-involutive p
+    = res
 
 ∈-resp-↭ : ∀ {x : A} → (x ∈_) Respects _↭_
 ∈-resp-↭ = Any-resp-↭
 
-Any-resp-[σ⁻¹∘σ] : {xs ys : List A} {P : Pred A p} →
-                   (σ : xs ↭ ys) →
-                   (ix : Any P xs) →
-                   Any-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix
-Any-resp-[σ⁻¹∘σ] refl          ix               = refl
-Any-resp-[σ⁻¹∘σ] (prep _ _)    (here _)         = refl
-Any-resp-[σ⁻¹∘σ] (swap _ _ _)  (here _)         = refl
-Any-resp-[σ⁻¹∘σ] (swap _ _ _)  (there (here _)) = refl
-Any-resp-[σ⁻¹∘σ] (trans σ₁ σ₂) ix
-  rewrite Any-resp-[σ⁻¹∘σ] σ₂ (Any-resp-↭ σ₁ ix)
-  rewrite Any-resp-[σ⁻¹∘σ] σ₁ ix
-  = refl
-Any-resp-[σ⁻¹∘σ] (prep _ σ)    (there ix)
-  rewrite Any-resp-[σ⁻¹∘σ] σ ix
-  = refl
-Any-resp-[σ⁻¹∘σ] (swap _ _ σ)  (there (there ix))
-  rewrite Any-resp-[σ⁻¹∘σ] σ ix
-  = refl
-
-∈-resp-[σ⁻¹∘σ] : {xs ys : List A} {x : A} →
-                 (σ : xs ↭ ys) →
-                 (ix : x ∈ xs) →
+∈-resp-[σ⁻¹∘σ] : ∀ {xs ys} {x : A} (σ : xs ↭ ys) (ix : x ∈ xs) →
                  ∈-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix
 ∈-resp-[σ⁻¹∘σ] = Any-resp-[σ⁻¹∘σ]
 
+∈-resp-[σ∘σ⁻¹] : ∀ {xs ys} {y : A} (σ : xs ↭ ys) (iy : y ∈ ys) →
+                 ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
+∈-resp-[σ∘σ⁻¹] = Any-resp-[σ∘σ⁻¹]
+
 ------------------------------------------------------------------------
 -- map
 
@@ -171,64 +182,63 @@ inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (prep v xs↭zs)) (++⁺ʳ _ ws↭ys
 shift : ∀ v (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
 shift v []       ys = refl
 shift v (x ∷ xs) ys = begin
-  x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v xs ys ⟩
-  x ∷ v ∷ xs ++ ys        <<⟨ refl ⟩
+  x ∷ (xs ++ [ v ] ++ ys) ↭⟨ prep _ (shift v xs ys) ⟩
+  x ∷ v ∷ xs ++ ys        ↭⟨ swap _ _ refl ⟩
   v ∷ x ∷ xs ++ ys        ∎
   where open PermutationReasoning
 
 drop-mid-≡ : ∀ {x : A} ws xs {ys} {zs} →
              ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ zs →
              ws ++ ys ↭ xs ++ zs
-drop-mid-≡ []       []       eq   with cong tail eq
-drop-mid-≡ []       []       eq   | refl = refl
+drop-mid-≡ []       []       eq
+  with refl ← List.∷-injectiveʳ eq = refl
 drop-mid-≡ []       (x ∷ xs) refl = shift _ xs _
 drop-mid-≡ (w ∷ ws) []       refl = ↭-sym (shift _ ws _)
-drop-mid-≡ (w ∷ ws) (x ∷ xs) eq with Lₚ.∷-injective eq
-... | refl , eq′ = prep w (drop-mid-≡ ws xs eq′)
+drop-mid-≡ (w ∷ ws) (x ∷ xs) eq
+  with refl , eq′ ← List.∷-injective eq = prep w (drop-mid-≡ ws xs eq′)
 
 drop-mid : ∀ {x : A} ws xs {ys zs} →
            ws ++ [ x ] ++ ys ↭ xs ++ [ x ] ++ zs →
            ws ++ ys ↭ xs ++ zs
-drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
+drop-mid ws xs p = drop-mid′ p ws xs refl refl
   where
-  drop-mid′ : ∀ {l′ l″ : List A} → l′ ↭ l″ →
-              ∀ ws xs {ys zs} →
-              ws ++ [ x ] ++ ys ≡ l′ →
-              xs ++ [ x ] ++ zs ≡ l″ →
+  drop-mid′ : ∀ {as bs} → as ↭ bs →
+              ∀ {x : A} ws xs {ys zs} →
+              as ≡ ws ++ [ x ] ++ ys →
+              bs ≡ xs ++ [ x ] ++ zs →
               ws ++ ys ↭ xs ++ zs
-  drop-mid′ refl         ws           xs           refl eq   = drop-mid-≡ ws xs (≡.sym eq)
-  drop-mid′ (prep x p)   []           []           refl eq   with cong tail eq
-  drop-mid′ (prep x p)   []           []           refl eq   | refl = p
+  drop-mid′ refl ws xs refl eq = drop-mid-≡ ws xs eq
+  drop-mid′ (trans p q) ws  xs refl refl
+    with h , t , refl ← ∈-∃++ (∈-resp-↭ p (∈-insert ws))
+    = trans (drop-mid ws h p) (drop-mid h xs q)
+  drop-mid′ (prep x p)   []           []           refl eq
+    with refl ← List.∷-injectiveʳ eq  = p
   drop-mid′ (prep x p)   []           (x ∷ xs)     refl refl = trans p (shift _ _ _)
   drop-mid′ (prep x p)   (w ∷ ws)     []           refl refl = trans (↭-sym (shift _ _ _)) p
-  drop-mid′ (prep x p)   (w ∷ ws)     (x ∷ xs)     refl refl = prep _ (drop-mid′ p ws xs refl refl)
+  drop-mid′ (prep x p)   (w ∷ ws)     (x ∷ xs)     refl refl = prep _ (drop-mid ws xs p)
   drop-mid′ (swap y z p) []           []           refl refl = prep _ p
-  drop-mid′ (swap y z p) []           (x ∷ [])     refl eq   with cong {B = List _}
-                                                                       (λ { (x ∷ _ ∷ xs) → x ∷ xs
-                                                                          ; _            → []
-                                                                          })
-                                                                       eq
-  drop-mid′ (swap y z p) []           (x ∷ [])     refl eq   | refl = prep _ p
+  drop-mid′ (swap y z p) []           (x ∷ [])     refl eq
+    with refl , eq′ ← List.∷-injective eq
+    with refl ← List.∷-injectiveʳ eq′ = prep _ p
   drop-mid′ (swap y z p) []           (x ∷ _ ∷ xs) refl refl = prep _ (trans p (shift _ _ _))
-  drop-mid′ (swap y z p) (w ∷ [])     []           refl eq   with cong tail eq
-  drop-mid′ (swap y z p) (w ∷ [])     []           refl eq   | refl = prep _ p
+  drop-mid′ (swap y z p) (w ∷ [])     []           refl eq
+    with refl ← List.∷-injectiveʳ eq  = prep _ p
   drop-mid′ (swap y z p) (w ∷ x ∷ ws) []           refl refl = prep _ (trans (↭-sym (shift _ _ _)) p)
   drop-mid′ (swap y y p) (y ∷ [])     (y ∷ [])     refl refl = prep _ p
   drop-mid′ (swap y z p) (y ∷ [])     (z ∷ y ∷ xs) refl refl = begin
-      _ ∷ _             <⟨ p ⟩
-      _ ∷ (xs ++ _ ∷ _) <⟨ shift _ _ _ ⟩
-      _ ∷ _ ∷ xs ++ _   <<⟨ refl ⟩
+      _ ∷ _             ↭⟨ prep _ p ⟩
+      _ ∷ (xs ++ _ ∷ _) ↭⟨ prep _ (shift _ _ _) ⟩
+      _ ∷ _ ∷ xs ++ _   ↭⟨ swap _ _ refl ⟩
       _ ∷ _ ∷ xs ++ _   ∎
       where open PermutationReasoning
   drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
-      _ ∷ _ ∷ ws ++ _   <<⟨ refl ⟩
-      _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩
-      _ ∷ (ws ++ _ ∷ _) <⟨ p ⟩
+      _ ∷ _ ∷ ws ++ _   ↭⟨ swap _ _ refl ⟩
+      _ ∷ (_ ∷ ws ++ _) ↭⟨ prep _ (shift _ _ _) ⟨
+      _ ∷ (ws ++ _ ∷ _) ↭⟨ prep _ p ⟩
       _ ∷ _             ∎
       where open PermutationReasoning
-  drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid′ p _ _ refl refl)
-  drop-mid′ (trans p₁ p₂) ws  xs refl refl with ∈-∃++ (∈-resp-↭ p₁ (∈-insert ws))
-  ... | (h , t , refl) = trans (drop-mid′ p₁ ws h refl refl) (drop-mid′ p₂ h xs refl refl)
+  drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid _ _ p)
+
 
 -- Algebraic properties
 
@@ -236,18 +246,18 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
 ++-identityˡ xs = refl
 
 ++-identityʳ : RightIdentity {A = List A} _↭_ [] _++_
-++-identityʳ xs = ↭-reflexive (Lₚ.++-identityʳ xs)
+++-identityʳ xs = ↭-reflexive (List.++-identityʳ xs)
 
 ++-identity : Identity {A = List A} _↭_ [] _++_
 ++-identity = ++-identityˡ , ++-identityʳ
 
 ++-assoc : Associative {A = List A} _↭_ _++_
-++-assoc xs ys zs = ↭-reflexive (Lₚ.++-assoc xs ys zs)
+++-assoc xs ys zs = ↭-reflexive (List.++-assoc xs ys zs)
 
 ++-comm : Commutative {A = List A} _↭_ _++_
 ++-comm []       ys = ↭-sym (++-identityʳ ys)
 ++-comm (x ∷ xs) ys = begin
-  x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
+  x ∷ xs ++ ys   ↭⟨ prep _ (++-comm xs ys) ⟩
   x ∷ ys ++ xs   ↭⟨ shift x ys xs ⟨
   ys ++ (x ∷ xs) ∎
   where open PermutationReasoning
@@ -320,7 +330,7 @@ drop-∷ = drop-mid [] []
 ∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
 ∷↭∷ʳ x xs = ↭-sym (begin
   xs ++ [ x ]   ↭⟨ shift x xs [] ⟩
-  x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
+  x ∷ xs ++ []  ≡⟨ List.++-identityʳ _ ⟩
   x ∷ xs        ∎)
   where open PermutationReasoning
 
@@ -337,7 +347,7 @@ drop-∷ = drop-mid [] []
 ↭-reverse : (xs : List A) → reverse xs ↭ xs
 ↭-reverse [] = ↭-refl
 ↭-reverse (x ∷ xs) = begin
-  reverse (x ∷ xs) ≡⟨ Lₚ.unfold-reverse x xs ⟩
+  reverse (x ∷ xs) ≡⟨ List.unfold-reverse x xs ⟩
   reverse xs ∷ʳ x ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨
   x ∷ reverse xs   ↭⟨ prep x (↭-reverse xs) ⟩
   x ∷ xs ∎
@@ -356,9 +366,9 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     with does (R? x y) | merge-↭ xs (y ∷ ys) | merge-↭ (x ∷ xs) ys
   ... | true  | rec | _   = prep x rec
   ... | false | _   | rec = begin
-    y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩
+    y ∷ merge R? (x ∷ xs) ys ↭⟨ prep _ rec ⟩
     y ∷ x ∷ xs ++ ys         ↭⟨ shift y (x ∷ xs) ys ⟨
-    (x ∷ xs) ++ y ∷ ys       ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨
+    (x ∷ xs) ++ y ∷ ys       ≡⟨ List.++-assoc [ x ] xs (y ∷ ys) ⟨
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
@@ -366,15 +376,10 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
 -- product
 
 product-↭ : product Preserves _↭_ ⟶ _≡_
-product-↭ refl = refl
-product-↭ (prep x r) = cong (x *_) (product-↭ r)
-product-↭ (trans r s) = ≡.trans (product-↭ r) (product-↭ s)
-product-↭ (swap {xs} {ys} x y r) = begin
-  x * (y * product xs) ≡˘⟨ *-assoc x y (product xs) ⟩
-  (x * y) * product xs ≡⟨ cong₂ _*_ (*-comm x y) (product-↭ r) ⟩
-  (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩
-  y * (x * product ys) ∎
-  where open ≡-Reasoning
+product-↭ p = foldr-commMonoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
+  where
+  module ℕ-*-1 = CommutativeMonoid ℕ.*-1-commutativeMonoid
+  open Permutation ℕ-*-1.setoid
 
 ------------------------------------------------------------------------
 -- catMaybes
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
new file mode 100644
index 0000000000..3bed7656fc
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
@@ -0,0 +1,54 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of permutation (with K)
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --with-K #-}
+
+module Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK where
+
+open import Function.Base using (_$_)
+open import Function.Bundles using (_⇔_; mk⇔)
+open import Function.Related.Propositional using (SK-sym; module EquationalReasoning)
+
+open import Data.List.Base using (deduplicate; _++_)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties using (++-∈⇔; deduplicate-∈⇔)
+open import Data.List.Membership.Propositional.Properties.WithK using (unique∧set⇒bag)
+open import Data.List.Relation.Unary.Unique.Propositional.Properties using (++⁺)
+open import Data.List.Relation.Binary.Disjoint.Propositional using (Disjoint)
+open import Data.List.Relation.Binary.Disjoint.Propositional.Properties
+  using (deduplicate⁺)
+open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
+open import Data.List.Relation.Binary.BagAndSetEquality using (∼bag⇒↭)
+
+open import Data.Sum as Sum using (_⊎_)
+open import Data.Sum.Function.Propositional using (_⊎-cong_)
+
+open import Relation.Binary.Definitions using (DecidableEquality)
+
+------------------------------------------------------------------------
+-- deduplicate
+
+module _ {a} {A : Set a} (_≟_ : DecidableEquality A) where
+
+  private
+    dedup≡   = deduplicate    _≟_
+    ∈-dedup≡ = deduplicate-∈⇔ _≟_
+
+  open import Data.List.Relation.Unary.Unique.DecPropositional.Properties _≟_
+    using (deduplicate-!)
+
+  dedup-++-↭ : ∀ {xs ys} → Disjoint xs ys → dedup≡ (xs ++ ys) ↭ dedup≡ xs ++ dedup≡ ys
+  dedup-++-↭ {xs} {ys} disj
+    = ∼bag⇒↭
+    $ unique∧set⇒bag
+        (deduplicate-! _)
+        (++⁺ (deduplicate-! _) (deduplicate-! _) (deduplicate⁺ _≟_ disj))
+    λ {x} → begin
+    x ∈ dedup≡ (xs ++ ys)           ∼⟨ SK-sym ∈-dedup≡ ⟩
+    x ∈ xs ++ ys                    ∼⟨ ++-∈⇔ ⟩
+    (x ∈ xs ⊎ x ∈ ys)               ∼⟨ ∈-dedup≡ ⊎-cong ∈-dedup≡ ⟩
+    (x ∈ dedup≡ xs ⊎ x ∈ dedup≡ ys) ∼⟨ SK-sym ++-∈⇔ ⟩
+    x ∈ dedup≡ xs ++ dedup≡ ys      ∎ where open EquationalReasoning
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 4409e78cc4..5c81eb6999 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -6,32 +6,29 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Function.Base using (_∘′_)
-open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Structures using (IsEquivalence)
-open import Relation.Binary.Definitions
-  using (Reflexive; Symmetric; Transitive)
-open import Relation.Binary.Reasoning.Syntax
 
 module Data.List.Relation.Binary.Permutation.Setoid
   {a ℓ} (S : Setoid a ℓ) where
 
 open import Data.List.Base using (List; _∷_)
 import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
-import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (refl)
-open import Data.List.Relation.Binary.Equality.Setoid S
-open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+import Data.List.Relation.Binary.Equality.Setoid as ≋
+open import Function.Base using (_∘′_)
 open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+open import Relation.Binary.Reasoning.Syntax
+open import Relation.Binary.Structures using (IsEquivalence)
 
-private
-  module Eq = Setoid S
-open Eq using (_≈_) renaming (Carrier to A)
+open module ≈ = Setoid S using (_≈_) renaming (Carrier to A)
+open ≋ S using (_≋_; _∷_; ≋-refl; ≋-sym; ≋-trans)
 
 ------------------------------------------------------------------------
--- Definition
+-- Definition, based on `Homogeneous`
 
 open Homogeneous public
   using (refl; prep; swap; trans)
@@ -41,47 +38,89 @@ infix 3 _↭_
 _↭_ : Rel (List A) (a ⊔ ℓ)
 _↭_ = Homogeneous.Permutation _≈_
 
+steps = Homogeneous.steps {R = _≈_}
+
 ------------------------------------------------------------------------
 -- Constructor aliases
 
+-- Constructor alias
+
+↭-reflexive-≋ : _≋_ ⇒ _↭_
+↭-reflexive-≋ = refl
+
+↭-trans : Transitive _↭_
+↭-trans = trans
+
 -- These provide aliases for `swap` and `prep` when the elements being
 -- swapped or prepended are propositionally equal
 
 ↭-prep : ∀ x {xs ys} → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-↭-prep x xs↭ys = prep Eq.refl xs↭ys
+↭-prep x xs↭ys = prep ≈.refl xs↭ys
 
 ↭-swap : ∀ x y {xs ys} → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
-↭-swap x y xs↭ys = swap Eq.refl Eq.refl xs↭ys
-
-------------------------------------------------------------------------
--- Functions over permutations
-
-steps : ∀ {xs ys} → xs ↭ ys → ℕ
-steps (refl _)            = 1
-steps (prep _ xs↭ys)      = suc (steps xs↭ys)
-steps (swap _ _ xs↭ys)    = suc (steps xs↭ys)
-steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs
+↭-swap x y xs↭ys = swap ≈.refl ≈.refl xs↭ys
 
 ------------------------------------------------------------------------
 -- _↭_ is an equivalence
 
 ↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl (Pointwise.refl Eq.refl)
+↭-reflexive refl = ↭-reflexive-≋ ≋-refl
 
 ↭-refl : Reflexive _↭_
 ↭-refl = ↭-reflexive refl
 
 ↭-sym : Symmetric _↭_
-↭-sym = Homogeneous.sym Eq.sym
+↭-sym = Homogeneous.sym ≈.sym
 
-↭-trans : Transitive _↭_
-↭-trans = trans
+-- As with the existing proofs `↭-respʳ-≋` and `↭-respˡ-≋` in `Setoid.Properties`
+-- (which appeal to symmetry of the underlying equality, and its effect on the
+-- proofs of symmetry for both pointwise equality and permutation) to the effect
+-- that _↭_ respects _≋_ on the left and right, such arguments can be both
+-- streamlined, and used to define a 'smart' constructor `↭-trans′` for transitivity.
+--
+-- The arguments below show how proofs of permutation can have all transitive
+-- compositions with instances of `refl` pushed to the leaves of derivations,
+-- thereby addressing the inefficiencies analysed in issue #1113
+--
+-- Conjecture: these transformations are `steps` invariant, but that is moot,
+-- given their use here, and in `Setoid.Properties.↭-split` (without requiring
+-- WF-induction on `steps`) to enable a new, sharper, analysis of lists `xs`
+-- such that `xs ↭ ys ++ [ x ] ++ zs` in terms of `x`, `ys`, and `zs`.
+
+↭-transˡ-≋ : LeftTrans _≋_ _↭_
+↭-transˡ-≋ xs≋ys               (refl ys≋zs)
+  = refl (≋-trans xs≋ys ys≋zs)
+↭-transˡ-≋ (x≈y ∷ xs≋ys)       (prep y≈z ys↭zs)
+  = prep (≈.trans x≈y y≈z) (↭-transˡ-≋ xs≋ys ys↭zs)
+↭-transˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ ys↭zs)
+  = swap (≈.trans x≈y eq₁) (≈.trans w≈z eq₂) (↭-transˡ-≋ xs≋ys ys↭zs)
+↭-transˡ-≋ xs≋ys               (trans ys↭ws ws↭zs)
+  = trans (↭-transˡ-≋ xs≋ys ys↭ws) ws↭zs
+
+↭-transʳ-≋ : RightTrans _↭_ _≋_
+↭-transʳ-≋ (refl xs≋ys)         ys≋zs
+  = refl (≋-trans xs≋ys ys≋zs)
+↭-transʳ-≋ (prep x≈y xs↭ys)     (y≈z ∷ ys≋zs)
+  = prep (≈.trans x≈y y≈z) (↭-transʳ-≋ xs↭ys ys≋zs)
+↭-transʳ-≋ (swap eq₁ eq₂ xs↭ys) (x≈w ∷ y≈z ∷ ys≋zs)
+  = swap (≈.trans eq₁ y≈z) (≈.trans eq₂ x≈w) (↭-transʳ-≋ xs↭ys ys≋zs)
+↭-transʳ-≋ (trans xs↭ws ws↭ys)  ys≋zs
+  = trans xs↭ws (↭-transʳ-≋ ws↭ys ys≋zs)
+
+↭-trans′ : Transitive _↭_
+↭-trans′ (refl xs≋ys) ys↭zs = ↭-transˡ-≋ xs≋ys ys↭zs
+↭-trans′ xs↭ys (refl ys≋zs) = ↭-transʳ-≋ xs↭ys ys≋zs
+↭-trans′ xs↭ys ys↭zs        = trans xs↭ys ys↭zs
 
 ↭-isEquivalence : IsEquivalence _↭_
-↭-isEquivalence = Homogeneous.isEquivalence Eq.refl Eq.sym
+↭-isEquivalence = record
+    { refl  = ↭-refl
+    ; sym   = ↭-sym
+    ; trans = ↭-trans
+    }
 
 ↭-setoid : Setoid _ _
-↭-setoid = Homogeneous.setoid {R = _≈_} Eq.refl Eq.sym
+↭-setoid = record { isEquivalence = ↭-isEquivalence }
 
 ------------------------------------------------------------------------
 -- A reasoning API to chain permutation proofs
@@ -95,7 +134,7 @@ module PermutationReasoning where
     renaming (≈-go to ↭-go)
 
   open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public
-  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ ↭-reflexive-≋) ≋-sym public
 
   -- Some extra combinators that allow us to skip certain elements
 
@@ -104,12 +143,12 @@ module PermutationReasoning where
   -- Skip reasoning on the first element
   step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
               xs ↭ ys → (x ∷ xs) IsRelatedTo zs
-  step-prep x xs rel xs↭ys = relTo (trans (prep Eq.refl xs↭ys) (begin rel))
+  step-prep x xs rel xs↭ys = ↭-go (↭-prep x xs↭ys) rel
 
   -- Skip reasoning about the first two elements
   step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
               xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
-  step-swap x y xs rel xs↭ys = relTo (trans (swap Eq.refl Eq.refl xs↭ys) (begin rel))
+  step-swap x y xs rel xs↭ys = ↭-go (↭-swap x y xs↭ys) rel
 
   syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
   syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 0440e3a3b6..d82178dd8b 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -16,7 +16,6 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties
   where
 
 open import Algebra
-import Algebra.Properties.CommutativeMonoid as ACM
 open import Data.Bool.Base using (true; false)
 open import Data.List.Base as List hiding (head; tail)
 open import Data.List.Relation.Binary.Pointwise as Pointwise
@@ -29,7 +28,7 @@ open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
 import Data.List.Relation.Unary.Unique.Setoid as Unique
 import Data.List.Membership.Setoid as Membership
 open import Data.List.Membership.Setoid.Properties using (∈-∃++; ∈-insert)
-import Data.List.Properties as Lₚ
+import Data.List.Properties as List
 open import Data.Nat.Base using (ℕ; suc; _<_; z<s; _+_)
 open import Data.Nat.Induction
 open import Data.Nat.Properties
@@ -37,36 +36,44 @@ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
 open import Function.Base using (_∘_; _⟨_⟩_; flip)
 open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred; Decidable)
-import Relation.Binary.Reasoning.Setoid as RelSetoid
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_)
 open import Relation.Nullary.Decidable using (yes; no; does)
 open import Relation.Nullary.Negation using (contradiction)
 
-private
-  variable
-    b p r : Level
 
-open Setoid S using (_≈_) renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
+open Setoid S using (_≈_)
+  renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
 open Permutation S
 open Membership S
 open Unique S using (Unique)
 open module ≋ = Equality S
-  using (_≋_; []; _∷_; ≋-refl; ≋-sym; ≋-trans; All-resp-≋; Any-resp-≋; AllPairs-resp-≋)
-open PermutationReasoning
+  using (_≋_; []; _∷_
+        ; ≋-refl; ≋-sym; ≋-trans
+        ; All-resp-≋; Any-resp-≋; AllPairs-resp-≋)
+
+private
+  variable
+    b p r : Level
+    x y z v w : A
+    xs ys zs vs ws : List A
+    P : Pred A p
+    R : Rel A r
+
 
 ------------------------------------------------------------------------
 -- Relationships to other predicates
 ------------------------------------------------------------------------
 
-All-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (All P) Respects _↭_
+All-resp-↭ : P Respects _≈_ → (All P) Respects _↭_
 All-resp-↭ resp (refl xs≋ys)   pxs             = All-resp-≋ resp xs≋ys pxs
 All-resp-↭ resp (prep x≈y p)   (px ∷ pxs)      = resp x≈y px ∷ All-resp-↭ resp p pxs
 All-resp-↭ resp (swap ≈₁ ≈₂ p) (px ∷ py ∷ pxs) = resp ≈₂ py ∷ resp ≈₁ px ∷ All-resp-↭ resp p pxs
 All-resp-↭ resp (trans p₁ p₂)  pxs             = All-resp-↭ resp p₂ (All-resp-↭ resp p₁ pxs)
 
-Any-resp-↭ : ∀ {P : Pred A p} → P Respects _≈_ → (Any P) Respects _↭_
+Any-resp-↭ : P Respects _≈_ → (Any P) Respects _↭_
 Any-resp-↭ resp (refl xs≋ys) pxs                 = Any-resp-≋ resp xs≋ys pxs
 Any-resp-↭ resp (prep x≈y p) (here px)           = here (resp x≈y px)
 Any-resp-↭ resp (prep x≈y p) (there pxs)         = there (Any-resp-↭ resp p pxs)
@@ -75,7 +82,7 @@ Any-resp-↭ resp (swap x y p) (there (here px))   = here (resp y px)
 Any-resp-↭ resp (swap x y p) (there (there pxs)) = there (there (Any-resp-↭ resp p pxs))
 Any-resp-↭ resp (trans p₁ p₂) pxs                = Any-resp-↭ resp p₂ (Any-resp-↭ resp p₁ pxs)
 
-AllPairs-resp-↭ : ∀ {R : Rel A r} → Symmetric R → R Respects₂ _≈_ → (AllPairs R) Respects _↭_
+AllPairs-resp-↭ : Symmetric R → R Respects₂ _≈_ → (AllPairs R) Respects _↭_
 AllPairs-resp-↭ sym resp (refl xs≋ys)     pxs             = AllPairs-resp-≋ resp xs≋ys pxs
 AllPairs-resp-↭ sym resp (prep x≈y p)     (∼ ∷ pxs)       =
   All-resp-↭ (proj₁ resp) p (All.map (proj₂ resp x≈y) ∼) ∷
@@ -87,100 +94,156 @@ AllPairs-resp-↭ sym resp@(rʳ , rˡ) (swap eq₁ eq₂ p) ((∼₁ ∷ ∼₂)
 AllPairs-resp-↭ sym resp (trans p₁ p₂)    pxs             =
   AllPairs-resp-↭ sym resp p₂ (AllPairs-resp-↭ sym resp p₁ pxs)
 
-∈-resp-↭ : ∀ {x} → (x ∈_) Respects _↭_
+∈-resp-↭ : (x ∈_) Respects _↭_
 ∈-resp-↭ = Any-resp-↭ (flip ≈-trans)
 
 Unique-resp-↭ : Unique Respects _↭_
 Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 
 ------------------------------------------------------------------------
--- Relationships to other relations
+-- Core properties depending on the representation of _↭_
 ------------------------------------------------------------------------
 
-≋⇒↭ : _≋_ ⇒ _↭_
-≋⇒↭ = refl
-
-↭-respʳ-≋ : _↭_ Respectsʳ _≋_
-↭-respʳ-≋ xs≋ys               (refl zs≋xs)         = refl (≋-trans zs≋xs xs≋ys)
-↭-respʳ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (≈-trans eq x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
-↭-respʳ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans eq₁ w≈z) (≈-trans eq₂ x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
-↭-respʳ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans ws↭zs (↭-respʳ-≋ xs≋ys zs↭xs)
-
-↭-respˡ-≋ : _↭_ Respectsˡ _≋_
-↭-respˡ-≋ xs≋ys               (refl ys≋zs)         = refl (≋-trans (≋-sym xs≋ys) ys≋zs)
-↭-respˡ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (≈-trans (≈-sym x≈y) eq) (↭-respˡ-≋ xs≋ys zs↭xs)
-↭-respˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans (≈-sym x≈y) eq₁) (≈-trans (≈-sym w≈z) eq₂) (↭-respˡ-≋ xs≋ys zs↭xs)
-↭-respˡ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans (↭-respˡ-≋ xs≋ys ws↭zs) zs↭xs
+shift : v ≈ w → ∀ xs ys → xs ++ [ v ] ++ ys ↭ w ∷ xs ++ ys
+shift {v} {w} v≈w []       ys = prep v≈w ↭-refl
+shift {v} {w} v≈w (x ∷ xs) ys = begin
+  x ∷ (xs ++ [ v ] ++ ys) ↭⟨ ↭-prep x (shift v≈w xs ys) ⟩
+  x ∷ w ∷ xs ++ ys        ↭⟨ ↭-swap x w ↭-refl ⟩
+  w ∷ x ∷ xs ++ ys        ∎
+  where open PermutationReasoning
 
 ------------------------------------------------------------------------
--- Properties of steps
+-- Relationship to `_≋_`
 ------------------------------------------------------------------------
 
-0<steps : ∀ {xs ys} (xs↭ys : xs ↭ ys) → 0 < steps xs↭ys
-0<steps (refl _)             = z<s
-0<steps (prep eq xs↭ys)      = m<n⇒m<1+n (0<steps xs↭ys)
-0<steps (swap eq₁ eq₂ xs↭ys) = m<n⇒m<1+n (0<steps xs↭ys)
-0<steps (trans xs↭ys xs↭ys₁) =
-  <-≤-trans (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁))
-
-steps-respˡ : ∀ {xs ys zs} (ys≋xs : ys ≋ xs) (ys↭zs : ys ↭ zs) →
-              steps (↭-respˡ-≋ ys≋xs ys↭zs) ≡ steps ys↭zs
-steps-respˡ _               (refl _)            = refl
-steps-respˡ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respˡ ys≋xs ys↭zs)
-steps-respˡ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respˡ ys≋xs ys↭zs)
-steps-respˡ ys≋xs           (trans ys↭ws ws↭zs) = cong (_+ steps ws↭zs) (steps-respˡ ys≋xs ys↭ws)
-
-steps-respʳ : ∀ {xs ys zs} (xs≋ys : xs ≋ ys) (zs↭xs : zs ↭ xs) →
-              steps (↭-respʳ-≋ xs≋ys zs↭xs) ≡ steps zs↭xs
-steps-respʳ _               (refl _)            = refl
-steps-respʳ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respʳ ys≋xs ys↭zs)
-steps-respʳ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respʳ ys≋xs ys↭zs)
-steps-respʳ ys≋xs           (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_) (steps-respʳ ys≋xs ws↭zs)
+↭-split : ∀ v as bs → xs ↭ (as ++ [ v ] ++ bs) →
+          ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs)
+                     × (ps ++ qs) ↭ (as ++ bs)
+↭-split v as bs p = helper as bs p ≋-refl
+  where
+  helper : ∀ as bs → xs ↭ ys → ys ≋ (as ++ [ v ] ++ bs) →
+           ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs)
+                      × (ps ++ qs) ↭ (as ++ bs)
+  helper as           bs (trans xs↭ys ys↭zs) zs≋as++[v]++ys
+    with ps , qs , eq , ↭ ← helper as bs ys↭zs zs≋as++[v]++ys
+    with ps′ , qs′ , eq′ , ↭′ ← helper ps qs xs↭ys eq
+    = ps′ , qs′ , eq′ , ↭-trans′ ↭′ ↭
+  helper []           _  (refl (x≈v ∷ xs≋vs)) (v≈y ∷ vs≋ys)
+    = [] , _ , ≈-trans x≈v v≈y ∷ ≋-refl , refl (≋-trans xs≋vs vs≋ys)
+  helper (a ∷ as)     bs (refl (x≈v ∷ xs≋vs)) (v≈y ∷ vs≋ys)
+    = _ ∷ as , bs , ≈-trans x≈v v≈y ∷ ≋-trans xs≋vs vs≋ys , ↭-refl
+  helper []           bs (prep {xs = xs} x≈v xs↭vs) (v≈y ∷ vs≋ys)
+    = [] , xs , ≈-trans x≈v v≈y ∷ ≋-refl , ↭-transʳ-≋ xs↭vs vs≋ys
+  helper (a ∷ as)     bs (prep x≈v as↭vs) (v≈y ∷ vs≋ys)
+    with ps , qs , eq , ↭ ← helper as bs as↭vs vs≋ys
+    = a ∷ ps , qs , ≈-trans x≈v v≈y ∷ eq , prep ≈-refl ↭
+  helper []           [] (swap _ _ _) (_ ∷ ())
+  helper []      (b ∷ _) (swap x≈v y≈w xs↭vs) (w≈z ∷ v≈y ∷ vs≋ys)
+    = b ∷ [] , _ , ≈-trans x≈v v≈y ∷ ≈-trans y≈w w≈z ∷ ≋-refl
+                 , ↭-prep b (↭-transʳ-≋ xs↭vs vs≋ys)
+  helper (a ∷ [])     bs (swap x≈v y≈w xs↭vs)  (w≈z ∷ v≈y ∷ vs≋ys)
+    = []     , a ∷ _ , ≈-trans x≈v v≈y ∷ ≈-trans y≈w w≈z ∷ ≋-refl
+                     , ↭-prep a (↭-transʳ-≋ xs↭vs vs≋ys)
+  helper (a ∷ b ∷ as) bs (swap x≈v y≈w as↭vs) (w≈a ∷ v≈b ∷ vs≋ys)
+    with ps , qs , eq , ↭ ← helper as bs as↭vs vs≋ys
+    = b ∷ a ∷ ps , qs , ≈-trans x≈v v≈b ∷ ≈-trans y≈w w≈a ∷ eq
+                      , ↭-swap _ _ ↭
 
 ------------------------------------------------------------------------
--- Properties of list functions
+-- Core properties of lists depending on the representation of _↭_
 ------------------------------------------------------------------------
 
 ------------------------------------------------------------------------
 -- map
 
-module _ {ℓ} (T : Setoid b ℓ) where
+module _ (T : Setoid b r) where
 
   open Setoid T using () renaming (_≈_ to _≈′_)
   open Permutation T using () renaming (_↭_ to _↭′_)
 
-  map⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ →
-         ∀ {xs ys} → xs ↭ ys → map f xs ↭′ map f ys
+  map⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ → (map f) Preserves _↭_ ⟶ _↭′_
   map⁺ pres (refl xs≋ys)  = refl (Pointwise.map⁺ _ _ (Pointwise.map pres xs≋ys))
   map⁺ pres (prep x p)    = prep (pres x) (map⁺ pres p)
   map⁺ pres (swap x y p)  = swap (pres x) (pres y) (map⁺ pres p)
   map⁺ pres (trans p₁ p₂) = trans (map⁺ pres p₁) (map⁺ pres p₂)
 
 ------------------------------------------------------------------------
--- _++_
+-- filter
 
-shift : ∀ {v w} → v ≈ w → (xs ys : List A) → xs ++ [ v ] ++ ys ↭ w ∷ xs ++ ys
-shift {v} {w} v≈w []       ys = prep v≈w ↭-refl
-shift {v} {w} v≈w (x ∷ xs) ys = begin
-  x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v≈w xs ys ⟩
-  x ∷ w ∷ xs ++ ys        <<⟨ ↭-refl ⟩
-  w ∷ x ∷ xs ++ ys        ∎
+module _ (P? : Decidable P) (P≈ : P Respects _≈_) where
 
-↭-shift : ∀ {v} (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
-↭-shift = shift ≈-refl
+  filter⁺ : ∀ {xs ys : List A} → xs ↭ ys → filter P? xs ↭ filter P? ys
+  filter⁺ (refl xs≋ys)        = refl (≋.filter⁺ P? P≈ xs≋ys)
+  filter⁺ (trans xs↭zs zs↭ys) = trans (filter⁺ xs↭zs) (filter⁺ zs↭ys)
+  filter⁺ {x ∷ xs} {y ∷ ys} (prep x≈y xs↭ys) with P? x | P? y
+  ... | yes _  | yes _  = prep x≈y (filter⁺ xs↭ys)
+  ... | yes Px | no ¬Py = contradiction (P≈ x≈y Px) ¬Py
+  ... | no ¬Px | yes Py = contradiction (P≈ (≈-sym x≈y) Py) ¬Px
+  ... | no  _  | no  _  = filter⁺ xs↭ys
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) with P? x | P? y
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | no ¬Py
+    with P? z | P? w
+  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
+  ... | yes Pz | _      = contradiction (P≈ (≈-sym x≈z) Pz) ¬Px
+  ... | no _   | no  _  = filter⁺ xs↭ys
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | yes Py
+    with P? z | P? w
+  ... | _      | no ¬Pw = contradiction (P≈ (≈-sym w≈y) Py) ¬Pw
+  ... | yes Pz | _      = contradiction (P≈ (≈-sym x≈z) Pz) ¬Px
+  ... | no _   | yes _  = prep w≈y (filter⁺ xs↭ys)
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys)  | yes Px | no ¬Py
+    with P? z | P? w
+  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
+  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
+  ... | yes _  | no _   = prep x≈z (filter⁺ xs↭ys)
+  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | yes Px | yes Py
+    with P? z | P? w
+  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
+  ... | _      | no ¬Pw = contradiction (P≈ (≈-sym w≈y) Py) ¬Pw
+  ... | yes _  | yes _  = swap x≈z w≈y (filter⁺ xs↭ys)
 
-++⁺ˡ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
-++⁺ˡ []       ys↭zs = ys↭zs
-++⁺ˡ (x ∷ xs) ys↭zs = ↭-prep _ (++⁺ˡ xs ys↭zs)
+------------------------------------------------------------------------
+-- _++_
 
-++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
+++⁺ʳ : ∀ zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
 ++⁺ʳ zs (refl xs≋ys)  = refl (Pointwise.++⁺ xs≋ys ≋-refl)
 ++⁺ʳ zs (prep x ↭)    = prep x (++⁺ʳ zs ↭)
 ++⁺ʳ zs (swap x y ↭)  = swap x y (++⁺ʳ zs ↭)
 ++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂)
 
+------------------------------------------------------------------------
+-- dropMiddleElement-≋
+
+dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
+           ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs →
+           ws ++ ys ↭ xs ++ zs
+dropMiddleElement-≋ []       []       (_   ∷ eq) = ↭-reflexive-≋ eq
+dropMiddleElement-≋ []       (x ∷ xs) (w≈v ∷ eq) = ↭-transˡ-≋ eq (shift w≈v xs _)
+dropMiddleElement-≋ (w ∷ ws) []       (w≈x ∷ eq) = ↭-transʳ-≋ (↭-sym (shift (≈-sym w≈x) ws _)) eq
+dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq) = prep w≈x (dropMiddleElement-≋ ws xs eq)
+
+------------------------------------------------------------------------
+-- Properties depending on the core properties of _↭_
+------------------------------------------------------------------------
+
+↭-shift : ∀ {v} xs ys → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
+↭-shift = shift ≈-refl
+
+++⁺ˡ : ∀ xs {ys zs} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
+++⁺ˡ []       ys↭zs = ys↭zs
+++⁺ˡ (x ∷ xs) ys↭zs = ↭-prep _ (++⁺ˡ xs ys↭zs)
+
 ++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
-++⁺ ws↭xs ys↭zs = trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
+++⁺ ws↭xs ys↭zs = ↭-trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
+
+-- Some other useful lemmas
+
+zoom : ∀ h {t xs ys} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
+zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t
+
+inject : ∀ v {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
+         ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
+inject v ws↭ys xs↭zs = ↭-trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _ ws↭ys)
 
 -- Algebraic properties
 
@@ -188,20 +251,31 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
 ++-identityˡ xs = ↭-refl
 
 ++-identityʳ : RightIdentity _↭_ [] _++_
-++-identityʳ xs = ↭-reflexive (Lₚ.++-identityʳ xs)
+++-identityʳ xs = ↭-reflexive (List.++-identityʳ xs)
 
 ++-identity : Identity _↭_ [] _++_
 ++-identity = ++-identityˡ , ++-identityʳ
 
 ++-assoc : Associative _↭_ _++_
-++-assoc xs ys zs = ↭-reflexive (Lₚ.++-assoc xs ys zs)
+++-assoc xs ys zs = ↭-reflexive (List.++-assoc xs ys zs)
 
 ++-comm : Commutative _↭_ _++_
 ++-comm []       ys = ↭-sym (++-identityʳ ys)
 ++-comm (x ∷ xs) ys = begin
-  x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
+  x ∷ xs ++ ys   ↭⟨ ↭-prep x (++-comm xs ys) ⟩
   x ∷ ys ++ xs   ↭⟨ ↭-shift ys xs ⟨
   ys ++ (x ∷ xs) ∎
+  where open PermutationReasoning
+
+-- Corollary
+
+shifts : ∀ xs ys {zs} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs
+shifts xs ys {zs} = begin
+   xs ++ ys  ++ zs ↭⟨ ++-assoc xs ys zs ⟨
+  (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩
+  (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
+   ys ++ xs  ++ zs ∎
+  where open PermutationReasoning
 
 -- Structures
 
@@ -251,123 +325,15 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
   { isCommutativeMonoid = ++-isCommutativeMonoid
   }
 
--- Some other useful lemmas
-
-zoom : ∀ h {t xs ys : List A} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
-zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t
-
-inject : ∀ (v : A) {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
-         ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
-inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _ ws↭ys)
-
-shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs
-shifts xs ys {zs} = begin
-   xs ++ ys  ++ zs ↭⟨ ++-assoc xs ys zs ⟨
-  (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩
-  (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
-   ys ++ xs  ++ zs ∎
-
-dropMiddleElement-≋ : ∀ {x} ws xs {ys} {zs} →
-           ws ++ [ x ] ++ ys ≋ xs ++ [ x ] ++ zs →
-           ws ++ ys ↭ xs ++ zs
-dropMiddleElement-≋ []       []       (_   ∷ eq) = ≋⇒↭ eq
-dropMiddleElement-≋ []       (x ∷ xs) (w≈v ∷ eq) = ↭-respˡ-≋ (≋-sym eq) (shift w≈v xs _)
-dropMiddleElement-≋ (w ∷ ws) []       (w≈x ∷ eq) = ↭-respʳ-≋ eq (↭-sym (shift (≈-sym w≈x) ws _))
-dropMiddleElement-≋ (w ∷ ws) (x ∷ xs) (w≈x ∷ eq) = prep w≈x (dropMiddleElement-≋ ws xs eq)
+------------------------------------------------------------------------
+-- dropMiddleElement, dropMiddle, and inversion for _∷_
 
 dropMiddleElement : ∀ {v} ws xs {ys zs} →
                     ws ++ [ v ] ++ ys ↭ xs ++ [ v ] ++ zs →
                     ws ++ ys ↭ xs ++ zs
-dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl
-  where
-  lemma : ∀ {w x y z} → w ≈ x → x ≈ y → z ≈ y → w ≈ z
-  lemma w≈x x≈y z≈y = ≈-trans (≈-trans w≈x x≈y) (≈-sym z≈y)
-
-  open PermutationReasoning
-
-  -- The l′ & l″ could be eliminated at the cost of making the `trans` case
-  -- much more difficult to prove. At the very least would require using `Acc`.
-  helper : ∀ {l′ l″ : List A} → l′ ↭ l″ →
-           ∀ ws xs {ys zs : List A} →
-           ws ++ [ v ] ++ ys ≋ l′ →
-           xs ++ [ v ] ++ zs ≋ l″ →
-           ws ++ ys ↭ xs ++ zs
-  helper {as}     {bs}     (refl eq3) ws xs {ys} {zs} eq1 eq2 =
-    dropMiddleElement-≋ ws xs (≋-trans (≋-trans eq1 eq3) (≋-sym eq2))
-  helper {_ ∷ as} {_ ∷ bs} (prep _ as↭bs) [] [] {ys} {zs} (_ ∷ ys≋as) (_ ∷ zs≋bs) = begin
-    ys               ≋⟨  ys≋as ⟩
-    as               ↭⟨  as↭bs ⟩
-    bs               ≋⟨ zs≋bs ⟨
-    zs               ∎
-  helper {_ ∷ as} {_ ∷ bs} (prep a≈b as↭bs) [] (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    ys               ≋⟨  ≋₁ ⟩
-    as               ↭⟨  as↭bs ⟩
-    bs               ≋⟨ ≋₂ ⟨
-    xs ++ v ∷ zs     ↭⟨  shift (lemma ≈₁ a≈b ≈₂) xs zs ⟩
-    x ∷ xs ++ zs     ∎
-  helper {_ ∷ as} {_ ∷ bs} (prep v≈w p) (w ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ ws ++ ys     ↭⟨  ↭-sym (shift (lemma ≈₂ (≈-sym v≈w) ≈₁) ws ys) ⟩
-    ws ++ v ∷ ys     ≋⟨  ≋₁ ⟩
-    as               ↭⟨  p ⟩
-    bs               ≋⟨ ≋₂ ⟨
-    zs               ∎
-  helper {_ ∷ as} {_ ∷ bs} (prep w≈x p) (w ∷ ws) (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ ws ++ ys     ↭⟨ prep (lemma ≈₁ w≈x ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩
-    x ∷ xs ++ zs     ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈x y≈v p) [] [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    ys               ≋⟨  ≋₁ ⟩
-    a ∷ as           ↭⟨  prep (≈-trans (≈-trans (≈-trans y≈v (≈-sym ≈₂)) ≈₁) v≈x) p ⟩
-    b ∷ bs           ≋⟨ ≋₂ ⟨
-    zs               ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈w p) [] (x ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    ys               ≋⟨  ≋₁ ⟩
-    a ∷ as           ↭⟨  prep y≈w p ⟩
-    _ ∷ bs           ≋⟨ ≈₂ ∷ tail ≋₂ ⟨
-    x ∷ zs           ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈x p) [] (x ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    ys               ≋⟨ ≋₁ ⟩
-    a ∷ as           ↭⟨ prep y≈x p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
-    x ∷ xs ++ v ∷ zs ↭⟨ prep ≈-refl (shift (lemma ≈₁ v≈w (head ≋₂)) xs zs) ⟩
-    x ∷ w ∷ xs ++ zs ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈x _ p) (w ∷ []) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ ys           ≋⟨ ≈₁ ∷ tail (≋₁) ⟩
-    _ ∷ as           ↭⟨ prep w≈x p ⟩
-    b ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
-    zs               ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈y x≈v p) (w ∷ x ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ x ∷ ws ++ ys ↭⟨ prep ≈-refl (↭-sym (shift (lemma ≈₂ (≈-sym x≈v) (head ≋₁)) ws ys)) ⟩
-    w ∷ ws ++ v ∷ ys ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep w≈y p ⟩
-    b ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
-    zs               ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap x≈v v≈y p) (x ∷ []) (y ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    x ∷ ys           ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep (≈-trans x≈v (≈-trans (≈-sym (head ≋₂)) (≈-trans (head ≋₁) v≈y))) p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
-    y ∷ zs           ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈w v≈z p) (y ∷ []) (z ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    y ∷ ys           ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep y≈w p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
-    w ∷ xs ++ v ∷ zs ↭⟨ ↭-prep w (↭-shift xs zs) ⟩
-    w ∷ v ∷ xs ++ zs ↭⟨ swap ≈-refl (lemma (head ≋₁) v≈z ≈₂) ↭-refl ⟩
-    z ∷ w ∷ xs ++ zs ∎
-  helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈v w≈z p) (y ∷ w ∷ ws) (z ∷ []) {ys} {zs}    (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    y ∷ w ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ y≈v (head ≋₂)) ≈-refl ↭-refl ⟩
-    w ∷ v ∷ ws ++ ys ↭⟨ ↭-prep w (↭-sym (↭-shift ws ys)) ⟩
-    w ∷ ws ++ v ∷ ys ≋⟨ ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep w≈z p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
-    z ∷ zs           ∎
-  helper (swap x≈z y≈w p) (x ∷ y ∷ ws) (w ∷ z ∷ xs) {ys} {zs} (≈₁ ∷ ≈₃ ∷ ≋₁) (≈₂ ∷ ≈₄ ∷ ≋₂) = begin
-    x ∷ y ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ x≈z ≈₄) (lemma ≈₃ y≈w ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩
-    w ∷ z ∷ xs ++ zs ∎
-  helper {as} {bs} (trans p₁ p₂) ws xs eq1 eq2
-    with ∈-∃++ S (∈-resp-↭ (↭-respˡ-≋ (≋-sym eq1) p₁) (∈-insert S ws ≈-refl))
-  ... | (h , t , w , v≈w , eq) = trans
-    (helper p₁ ws h eq1 (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq)))
-    (helper p₂ h xs (≋-trans (≋.++⁺ ≋-refl (v≈w ∷ ≋-refl)) (≋-sym eq)) eq2)
+dropMiddleElement {v} ws xs {ys} {zs} p =
+  let ps , qs , eq , ↭ = ↭-split v xs zs p
+  in ↭-trans (dropMiddleElement-≋ ws ps eq) ↭
 
 dropMiddle : ∀ {vs} ws xs {ys zs} →
              ws ++ vs ++ ys ↭ xs ++ vs ++ zs →
@@ -375,64 +341,42 @@ dropMiddle : ∀ {vs} ws xs {ys zs} →
 dropMiddle {[]}     ws xs p = p
 dropMiddle {v ∷ vs} ws xs p = dropMiddle ws xs (dropMiddleElement ws xs p)
 
-split : ∀ (v : A) as bs {xs} → xs ↭ as ++ [ v ] ++ bs → ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
-split v as bs p = helper as bs p (<-wellFounded (steps p))
-  where
-  helper : ∀ as bs {xs} (p : xs ↭ as ++ [ v ] ++ bs) → Acc _<_ (steps p) →
-           ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
-  helper []           bs (refl eq)    _ = []         , bs , eq
-  helper (a ∷ [])     bs (refl eq)    _ = [ a ]      , bs , eq
-  helper (a ∷ b ∷ as) bs (refl eq)    _ = a ∷ b ∷ as , bs , eq
-  helper []           bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl
-  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
-  ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂
-  helper [] (b ∷ bs)     (swap x≈b y≈v _) _ = [ b ] , _     , x≈b ∷ y≈v ∷ ≋-refl
-  helper (a ∷ [])     bs (swap x≈v y≈a ↭) _ = []    , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl
-  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
-  ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq
-  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec (m<n+m (steps ↭₂) (0<steps ↭₁)))
-  ... | (ps , qs , eq) = helper ps qs (↭-respʳ-≋ eq ↭₁)
-      (rec (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
+drop-∷ : x ∷ xs ↭ x ∷ ys → xs ↭ ys
+drop-∷ = dropMiddleElement [] []
 
 ------------------------------------------------------------------------
--- filter
+-- _∷ʳ_
 
-module _ {p} {P : Pred A p} (P? : Decidable P) (P≈ : P Respects _≈_) where
+∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
+∷↭∷ʳ x xs = ↭-sym (begin
+  xs ++ [ x ]   ↭⟨ ↭-shift xs [] ⟩
+  x ∷ xs ++ []  ≡⟨ List.++-identityʳ _ ⟩
+  x ∷ xs        ∎)
+  where open PermutationReasoning
 
-  filter⁺ : ∀ {xs ys : List A} → xs ↭ ys → filter P? xs ↭ filter P? ys
-  filter⁺ (refl xs≋ys)        = refl (≋.filter⁺ P? P≈ xs≋ys)
-  filter⁺ (trans xs↭zs zs↭ys) = trans (filter⁺ xs↭zs) (filter⁺ zs↭ys)
-  filter⁺ {x ∷ xs} {y ∷ ys} (prep x≈y xs↭ys) with P? x | P? y
-  ... | yes _  | yes _  = prep x≈y (filter⁺ xs↭ys)
-  ... | yes Px | no ¬Py = contradiction (P≈ x≈y Px) ¬Py
-  ... | no ¬Px | yes Py = contradiction (P≈ (≈-sym x≈y) Py) ¬Px
-  ... | no  _  | no  _  = filter⁺ xs↭ys
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) with P? x | P? y
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | no ¬Py
-    with P? z | P? w
-  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
-  ... | yes Pz | _      = contradiction (P≈ (≈-sym x≈z) Pz) ¬Px
-  ... | no _   | no  _  = filter⁺ xs↭ys
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | no ¬Px | yes Py
-    with P? z | P? w
-  ... | _      | no ¬Pw = contradiction (P≈ (≈-sym w≈y) Py) ¬Pw
-  ... | yes Pz | _      = contradiction (P≈ (≈-sym x≈z) Pz) ¬Px
-  ... | no _   | yes _  = prep w≈y (filter⁺ xs↭ys)
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys)  | yes Px | no ¬Py
-    with P? z | P? w
-  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
-  ... | _      | yes Pw = contradiction (P≈ w≈y Pw) ¬Py
-  ... | yes _  | no _   = prep x≈z (filter⁺ xs↭ys)
-  filter⁺ {x ∷ w ∷ xs} {y ∷ z ∷ ys} (swap x≈z w≈y xs↭ys) | yes Px | yes Py
-    with P? z | P? w
-  ... | no ¬Pz | _      = contradiction (P≈ x≈z Px) ¬Pz
-  ... | _      | no ¬Pw = contradiction (P≈ (≈-sym w≈y) Py) ¬Pw
-  ... | yes _  | yes _  = swap x≈z w≈y (filter⁺ xs↭ys)
+------------------------------------------------------------------------
+-- reverse
+
+↭-reverse : (xs : List A) → reverse xs ↭ xs
+↭-reverse [] = ↭-refl
+↭-reverse (x ∷ xs) = begin
+  reverse (x ∷ xs) ≡⟨ List.unfold-reverse x xs ⟩
+  reverse xs ∷ʳ x  ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨
+  x ∷ reverse xs   ↭⟨ ↭-prep x (↭-reverse xs) ⟩
+  x ∷ xs           ∎
+  where open PermutationReasoning
+
+------------------------------------------------------------------------
+-- ʳ++
+
+++↭ʳ++ : ∀ (xs ys : List A) → xs ++ ys ↭ xs ʳ++ ys
+++↭ʳ++ []       ys = ↭-refl
+++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys))
 
 ------------------------------------------------------------------------
 -- partition
 
-module _ {p} {P : Pred A p} (P? : Decidable P) where
+module _ (P? : Decidable P) where
 
   partition-↭ : ∀ xs → (let ys , zs = partition P? xs) → xs ↭ ys ++ zs
   partition-↭ []       = ↭-refl
@@ -444,7 +388,7 @@ module _ {p} {P : Pred A p} (P? : Decidable P) where
 ------------------------------------------------------------------------
 -- merge
 
-module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where
+module _ (R? : B.Decidable R) where
 
   merge-↭ : ∀ xs ys → merge R? xs ys ↭ xs ++ ys
   merge-↭ []       []       = ↭-refl
@@ -454,52 +398,96 @@ module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where
     with does (R? x y) | merge-↭ xs (y ∷ ys) | merge-↭ (x ∷ xs) ys
   ... | true  | rec | _   = ↭-prep x rec
   ... | false | _   | rec = begin
-    y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩
+    y ∷ merge R? (x ∷ xs) ys ↭⟨ ↭-prep _ rec ⟩
     y ∷ x ∷ xs ++ ys         ↭⟨ ↭-shift (x ∷ xs) ys ⟨
-    (x ∷ xs) ++ y ∷ ys       ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨
+    (x ∷ xs) ++ y ∷ ys       ≡⟨ List.++-assoc [ x ] xs (y ∷ ys) ⟨
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
 
 ------------------------------------------------------------------------
--- _∷ʳ_
+-- foldr over a Commutative Monoid
 
-∷↭∷ʳ : ∀ (x : A) xs → x ∷ xs ↭ xs ∷ʳ x
-∷↭∷ʳ x xs = ↭-sym (begin
-  xs ++ [ x ]   ↭⟨ ↭-shift xs [] ⟩
-  x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
-  x ∷ xs        ∎)
-  where open PermutationReasoning
+module _{_∙_ : Op₂ A} {ε : A}
+        (isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε) where
 
-------------------------------------------------------------------------
--- ʳ++
+  private
+    commutativeMonoid : CommutativeMonoid _ _
+    commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
+    open module CM = CommutativeMonoid commutativeMonoid
+      using (∙-cong; ∙-congˡ; ∙-congʳ; assoc; comm)
+
+  foldr-commMonoid : (foldr _∙_ ε) Preserves _↭_ ⟶ _≈_
+  foldr-commMonoid (refl xs≋ys)        = Pointwise.foldr⁺ ∙-cong CM.refl xs≋ys
+  foldr-commMonoid (prep x≈y xs↭ys)    = ∙-cong x≈y (foldr-commMonoid xs↭ys)
+  foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = begin
+    x ∙ (y ∙ foldr _∙_ ε xs)    ≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩
+    x ∙ (y ∙ foldr _∙_ ε ys)    ≈⟨ assoc x y (foldr _∙_ ε ys) ⟨
+    (x ∙ y) ∙ foldr _∙_ ε ys    ≈⟨ ∙-congʳ (comm x y) ⟩
+    (y ∙ x) ∙ foldr _∙_ ε ys    ≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩
+    (y′ ∙ x′) ∙ foldr _∙_ ε ys  ≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩
+    y′ ∙ (x′ ∙ foldr _∙_ ε ys)  ∎
+    where open ≈-Reasoning CM.setoid
+  foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)
 
-++↭ʳ++ : ∀ (xs ys : List A) → xs ++ ys ↭ xs ʳ++ ys
-++↭ʳ++ []       ys = ↭-refl
-++↭ʳ++ (x ∷ xs) ys = ↭-trans (↭-sym (↭-shift xs ys)) (++↭ʳ++ xs (x ∷ ys))
 
 ------------------------------------------------------------------------
--- foldr of Commutative Monoid
+-- TOWARDS DEPRECATION
+------------------------------------------------------------------------
 
-module _ {_∙_ : Op₂ A} {ε : A} (isCmonoid : IsCommutativeMonoid _≈_ _∙_ ε) where
-  open module CM = IsCommutativeMonoid isCmonoid
+≋⇒↭ = ↭-reflexive-≋
 
-  private
-    module S = RelSetoid setoid
-
-    cmonoid : CommutativeMonoid _ _
-    cmonoid = record { isCommutativeMonoid = isCmonoid }
-
-  open ACM cmonoid
-
-  foldr-commMonoid : ∀ {xs ys} → xs ↭ ys → foldr _∙_ ε xs ≈ foldr _∙_ ε ys
-  foldr-commMonoid (refl []) = CM.refl
-  foldr-commMonoid (refl (x≈y ∷ xs≈ys)) = ∙-cong x≈y (foldr-commMonoid (Permutation.refl xs≈ys))
-  foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys)
-  foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = S.begin
-    x ∙ (y ∙ foldr _∙_ ε xs)   S.≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩
-    x ∙ (y ∙ foldr _∙_ ε ys)   S.≈⟨ assoc x y (foldr _∙_ ε ys) ⟨
-    (x ∙ y) ∙ foldr _∙_ ε ys   S.≈⟨ ∙-congʳ (comm x y) ⟩
-    (y ∙ x) ∙ foldr _∙_ ε ys   S.≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩
-    (y′ ∙ x′) ∙ foldr _∙_ ε ys S.≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩
-    y′ ∙ (x′ ∙ foldr _∙_ ε ys) S.∎
-  foldr-commMonoid (trans xs↭ys ys↭zs) = CM.trans (foldr-commMonoid xs↭ys) (foldr-commMonoid ys↭zs)
+-- These are easily superseded by ↭-transˡ-≋, ↭-transʳ-≋
+-- But for the properties of steps which require precise measurement
+
+↭-respʳ-≋ : _↭_ Respectsʳ _≋_
+↭-respʳ-≋ xs≋ys               (refl zs≋xs)         = refl (≋-trans zs≋xs xs≋ys)
+↭-respʳ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (≈-trans eq x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
+↭-respʳ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans eq₁ w≈z) (≈-trans eq₂ x≈y) (↭-respʳ-≋ xs≋ys zs↭xs)
+↭-respʳ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans ws↭zs (↭-respʳ-≋ xs≋ys zs↭xs)
+
+↭-respˡ-≋ : _↭_ Respectsˡ _≋_
+↭-respˡ-≋ xs≋ys               (refl ys≋zs)         = refl (≋-trans (≋-sym xs≋ys) ys≋zs)
+↭-respˡ-≋ (x≈y ∷ xs≋ys)       (prep eq zs↭xs)      = prep (≈-trans (≈-sym x≈y) eq) (↭-respˡ-≋ xs≋ys zs↭xs)
+↭-respˡ-≋ (x≈y ∷ w≈z ∷ xs≋ys) (swap eq₁ eq₂ zs↭xs) = swap (≈-trans (≈-sym x≈y) eq₁) (≈-trans (≈-sym w≈z) eq₂) (↭-respˡ-≋ xs≋ys zs↭xs)
+↭-respˡ-≋ xs≋ys               (trans ws↭zs zs↭xs)  = trans (↭-respˡ-≋ xs≋ys ws↭zs) zs↭xs
+
+-- Properties of steps using the above
+
+0<steps : (xs↭ys : xs ↭ ys) → 0 < steps xs↭ys
+0<steps (refl _)             = z<s
+0<steps (prep eq xs↭ys)      = m<n⇒m<1+n (0<steps xs↭ys)
+0<steps (swap eq₁ eq₂ xs↭ys) = m<n⇒m<1+n (0<steps xs↭ys)
+0<steps (trans xs↭ys xs↭ys₁) =
+  <-≤-trans (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁))
+
+steps-respˡ : (ys≋xs : ys ≋ xs) (ys↭zs : ys ↭ zs) →
+              steps (↭-respˡ-≋ ys≋xs ys↭zs) ≡ steps ys↭zs
+steps-respˡ _               (refl _)            = refl
+steps-respˡ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respˡ ys≋xs ys↭zs)
+steps-respˡ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respˡ ys≋xs ys↭zs)
+steps-respˡ ys≋xs           (trans ys↭ws ws↭zs) = cong (_+ steps ws↭zs) (steps-respˡ ys≋xs ys↭ws)
+
+steps-respʳ : (xs≋ys : xs ≋ ys) (zs↭xs : zs ↭ xs) →
+              steps (↭-respʳ-≋ xs≋ys zs↭xs) ≡ steps zs↭xs
+steps-respʳ _               (refl _)            = refl
+steps-respʳ (_ ∷ ys≋xs)     (prep _ ys↭zs)      = cong suc (steps-respʳ ys≋xs ys↭zs)
+steps-respʳ (_ ∷ _ ∷ ys≋xs) (swap _ _ ys↭zs)    = cong suc (steps-respʳ ys≋xs ys↭zs)
+steps-respʳ ys≋xs           (trans ys↭ws ws↭zs) = cong (steps ys↭ws +_) (steps-respʳ ys≋xs ws↭zs)
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+split : ∀ (v : A) as bs {xs} → xs ↭ as ++ [ v ] ++ bs →
+        ∃₂ λ ps qs → xs ≋ ps ++ [ v ] ++ qs
+split v as bs xs↭as++[v]++bs
+  with ps , qs , eq , _ ← ↭-split v as bs xs↭as++[v]++bs
+  = ps , qs , eq
+{-# WARNING_ON_USAGE split
+"Warning: split was deprecated in v2.1.
+Please use the sharper lemma ↭-split instead."
+#-}
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
index 8dd94d8b3b..77c2ef5738 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
@@ -331,10 +331,14 @@ module _ {R : REL A B r} where
   ∷ʳ⁻¹ ¬r = mk⇔ (_ ∷ʳ_) (∷ʳ⁻ ¬r)
 
 ------------------------------------------------------------------------
--- Irrelevant special case
+-- Empty special case
 
 module _ {R : REL A B r} where
 
+  Sublist-[]-universal : U.Universal (Sublist R [])
+  Sublist-[]-universal []      = []
+  Sublist-[]-universal (_ ∷ _) = _ ∷ʳ Sublist-[]-universal _
+
   Sublist-[]-irrelevant : U.Irrelevant (Sublist R [])
   Sublist-[]-irrelevant []       []        = ≡.refl
   Sublist-[]-irrelevant (y ∷ʳ p) (.y ∷ʳ q) = ≡.cong (y ∷ʳ_) (Sublist-[]-irrelevant p q)
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index 60be70aac1..b42e33365d 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -24,7 +24,7 @@ open import Level
 open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; cong; cong₂)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
-open import Relation.Unary using (Pred; Decidable; Irrelevant)
+open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable using (¬?; yes; no)
 
@@ -293,7 +293,10 @@ module _ where
   to-≋ = HeteroProperties.toPointwise
 
 ------------------------------------------------------------------------
--- Irrelevant special case
+-- Empty special case
+
+  []⊆-universal : Universal ([] ⊆_)
+  []⊆-universal = HeteroProperties.Sublist-[]-universal
 
   []⊆-irrelevant : Irrelevant ([] ⊆_)
   []⊆-irrelevant = HeteroProperties.Sublist-[]-irrelevant
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
index 75e1a5b00a..4054afc092 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -10,25 +10,25 @@ module Data.List.Relation.Binary.Subset.Propositional.Properties
   where
 
 open import Data.Bool.Base using (Bool; true; false; T)
-open import Data.List.Base using (List; map; _∷_; _++_; concat; applyUpTo;
-  any; filter)
+open import Data.List.Base
+  using (List; []; map; _∷_; _++_; concat; concatMap; applyUpTo; any; filter)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All)
 import Data.List.Relation.Unary.Any.Properties as Any hiding (filter⁺)
 open import Data.List.Effectful using (monad)
 open import Data.List.Relation.Unary.Any using (Any)
-open import Data.List.Membership.Propositional using (_∈_; mapWith∈)
+open import Data.List.Membership.Propositional using (_∈_; _∉_; mapWith∈)
 open import Data.List.Membership.Propositional.Properties
   using (map-∈↔; concat-∈↔; >>=-∈↔; ⊛-∈↔; ⊗-∈↔)
 import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset
 open import Data.List.Relation.Binary.Subset.Propositional
-  using (_⊆_; _⊇_)
+  using (_⊆_; _⊇_; _⊈_)
 open import Data.List.Relation.Binary.Permutation.Propositional
   using (_↭_; ↭-sym; ↭-isEquivalence)
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation
 open import Data.Nat.Base using (ℕ; _≤_)
 import Data.Product.Base as Product
-import Data.Sum.Base as Sum
+open import Data.Sum.Base as Sum using (_⊎_)
 open import Effect.Monad
 open import Function.Base using (_∘_; _∘′_; id; _$_)
 open import Function.Bundles using (_↔_; Inverse; Equivalence)
@@ -52,8 +52,19 @@ private
     a b p q : Level
     A : Set a
     B : Set b
+    x y : A
     ws xs ys zs : List A
 
+------------------------------------------------------------------------
+-- Basics
+------------------------------------------------------------------------
+
+∷⊈[] : x ∷ xs ⊈ []
+∷⊈[] = Subset.∷⊈[] (setoid _)
+
+⊆[]⇒≡[] : ∀ {A : Set a} → (_⊆ []) ⋐ (_≡ [])
+⊆[]⇒≡[] {A = A} = Subset.⊆[]⇒≡[] (setoid A)
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -150,6 +161,12 @@ xs⊆x∷xs = Subset.xs⊆x∷xs (setoid _)
 ∈-∷⁺ʳ : ∀ {x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
 ∈-∷⁺ʳ = Subset.∈-∷⁺ʳ (setoid _)
 
+⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+⊆∷⇒∈∨⊆ = Subset.⊆∷⇒∈∨⊆ (setoid _)
+
+⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+⊆∷∧∉⇒⊆ = Subset.⊆∷∧∉⇒⊆ (setoid _)
+
 ------------------------------------------------------------------------
 -- _++_
 
@@ -179,6 +196,12 @@ module _ {xss yss : List (List A)} where
     Product.map₂ (Product.map₂ xss⊆yss) ∘
     Inverse.from concat-∈↔
 
+------------------------------------------------------------------------
+-- concatMap
+
+concatMap⁺ : ∀ (f : A → List B) → xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
+concatMap⁺ _ = concat⁺ ∘ map⁺ _
+
 ------------------------------------------------------------------------
 -- applyUpTo
 
diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
index 0d0d685a27..901ee8b942 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
@@ -22,7 +22,8 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Binary.Permutation.Setoid as Permutation
 import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutationₚ
 open import Data.Product.Base using (_,_)
-open import Function.Base using (_∘_; _∘₂_; _$_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Function.Base using (_∘_; _∘₂_; _$_; case_of_)
 open import Level using (Level)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
@@ -34,6 +35,7 @@ open import Relation.Binary.Bundles using (Setoid; Preorder)
 open import Relation.Binary.Structures using (IsPreorder)
 import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
 open import Relation.Binary.Reasoning.Syntax
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 open Setoid using (Carrier)
 
@@ -41,6 +43,22 @@ private
   variable
     a b p q r ℓ : Level
 
+------------------------------------------------------------------------
+-- Basics
+------------------------------------------------------------------------
+
+module _ (S : Setoid a ℓ) where
+
+  open Setoid S using (refl)
+  open Subset S
+
+  ∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
+  ∷⊈[] p = Membershipₚ.∉[] S $ p (here refl)
+
+  ⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ [])
+  ⊆[]⇒≡[] {x = []}    _ = ≡.refl
+  ⊆[]⇒≡[] {x = _ ∷ _} p with () ← ∷⊈[] p
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -161,12 +179,14 @@ module _ (S : Setoid a ℓ) where
 
 ------------------------------------------------------------------------
 -- Properties of list functions
+------------------------------------------------------------------------
+
 ------------------------------------------------------------------------
 -- ∷
 
 module _ (S : Setoid a ℓ) where
 
-  open Setoid S
+  open Setoid S renaming (Carrier to A)
   open Subset S
   open Membership S
   open Membershipₚ
@@ -174,14 +194,31 @@ module _ (S : Setoid a ℓ) where
   xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs
   xs⊆x∷xs xs x = there
 
-  ∷⁺ʳ : ∀ {xs ys} x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
+  private variable
+    x y : A
+    xs ys : List A
+
+  ∷⁺ʳ : ∀ x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
   ∷⁺ʳ x xs⊆ys (here  p) = here p
   ∷⁺ʳ x xs⊆ys (there p) = there (xs⊆ys p)
 
-  ∈-∷⁺ʳ : ∀ {xs ys x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
+  ∈-∷⁺ʳ : x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
   ∈-∷⁺ʳ x∈ys _  (here  v≈x)  = ∈-resp-≈ S (sym v≈x) x∈ys
   ∈-∷⁺ʳ _ xs⊆ys (there x∈xs) = xs⊆ys x∈xs
 
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷⇒∈∨⊆ {xs = []}       []⊆y∷ys = inj₂ λ ()
+  ⊆∷⇒∈∨⊆ {xs = _ ∷ _} x∷xs⊆y∷ys with ⊆∷⇒∈∨⊆ $ x∷xs⊆y∷ys ∘ there
+  ... | inj₁ y∈xs  = inj₁ $ there y∈xs
+  ... | inj₂ xs⊆ys with x∷xs⊆y∷ys (here refl)
+  ...   | here x≈y = inj₁ $ here (sym x≈y)
+  ...   | there x∈ys = inj₂ (∈-∷⁺ʳ x∈ys xs⊆ys)
+
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ⊆∷∧∉⇒⊆ xs⊆y∷ys y∉xs with ⊆∷⇒∈∨⊆ xs⊆y∷ys
+  ... | inj₁ y∈xs  = contradiction y∈xs y∉xs
+  ... | inj₂ xs⊆ys = xs⊆ys
+
 ------------------------------------------------------------------------
 -- ++
 
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 836e73d4a4..6f1df8cbcc 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -461,6 +461,17 @@ module _ {P : A → Set p} where
   concat↔ : ∀ {xss} → Any (Any P) xss ↔ Any P (concat xss)
   concat↔ {xss} = mk↔ₛ′ concat⁺ (concat⁻ xss) (concat⁺∘concat⁻ xss) concat⁻∘concat⁺
 
+------------------------------------------------------------------------
+-- concatMap
+
+module _ (f : A → List B) {p} {P : Pred B p} where
+
+  concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
+  concatMap⁺ = concat⁺ ∘ map⁺
+
+  concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
+  concatMap⁻ = map⁻ ∘ concat⁻ _
+
 ------------------------------------------------------------------------
 -- cartesianProductWith
 
diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
index bcd7df1176..8852bdd704 100644
--- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
@@ -8,9 +8,12 @@
 
 module Data.List.Relation.Unary.Unique.Propositional.Properties where
 
-open import Data.List.Base using (map; _++_; concat; cartesianProductWith;
-  cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom;
-  tabulate; allFin; filter)
+open import Data.List.Base
+  using ( List; _∷_; map; _++_; concat; cartesianProductWith
+        ; cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom
+        ; tabulate; allFin; filter
+        )
+open import Data.List.Membership.Propositional using (_∉_)
 open import Data.List.Relation.Binary.Disjoint.Propositional
   using (Disjoint)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
@@ -35,6 +38,9 @@ open import Relation.Nullary.Negation using (¬_)
 private
   variable
     a b c p : Level
+    A : Set a
+    x y : A
+    xs : List A
 
 ------------------------------------------------------------------------
 -- Introduction (⁺) and elimination (⁻) rules for list operations
@@ -154,3 +160,9 @@ module _ {A : Set a} {P : Pred _ p} (P? : Decidable P) where
 
   filter⁺ : ∀ {xs} → Unique xs → Unique (filter P? xs)
   filter⁺ = Setoid.filter⁺ (setoid A) P?
+
+------------------------------------------------------------------------
+-- ∷
+
+Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
+Unique[x∷xs]⇒x∉xs = Setoid.Unique[x∷xs]⇒x∉xs (setoid _)
diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
index ffb587018a..0dc7027c79 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
@@ -9,9 +9,11 @@
 module Data.List.Relation.Unary.Unique.Setoid.Properties where
 
 open import Data.List.Base
+import Data.List.Membership.Setoid as Membership
 open import Data.List.Membership.Setoid.Properties
 open import Data.List.Relation.Binary.Disjoint.Setoid
 open import Data.List.Relation.Binary.Disjoint.Setoid.Properties
+open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any)
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
@@ -156,3 +158,21 @@ module _ (S : Setoid a ℓ) {P : Pred _ p} (P? : Decidable P) where
 
   filter⁺ : ∀ {xs} → Unique S xs → Unique S (filter P? xs)
   filter⁺ = AllPairs.filter⁺ P?
+
+------------------------------------------------------------------------
+-- ∷
+
+module _ (S : Setoid a ℓ) where
+
+  open Setoid S renaming (Carrier to A)
+  open Membership S using (_∉_)
+
+  private
+    variable
+      x y : A
+      xs : List A
+
+  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
+  Unique[x∷xs]⇒x∉xs ((x≉ ∷ x∉) ∷ _ ∷ uniq) = λ where
+    (here x≈)  → x≉ x≈
+    (there x∈) → Unique[x∷xs]⇒x∉xs (x∉ AllPairs.∷ uniq) x∈
diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda
index a954dc99ec..50b75b309d 100644
--- a/src/Relation/Binary/Construct/Interior/Symmetric.agda
+++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda
@@ -8,15 +8,18 @@
 
 module Relation.Binary.Construct.Interior.Symmetric where
 
-open import Function.Base using (flip)
-open import Level
+open import Data.Bool.Base using (_∧_)
+open import Function.Base using (flip; _∘_)
+open import Level using (Level)
 open import Relation.Binary
+open import Relation.Nullary.Decidable.Core
+open import Relation.Nullary.Reflects
 
 private
   variable
-    a b c ℓ r s t : Level
+    a ℓ : Level
     A : Set a
-    R S T : Rel A r
+    R S T : Rel A ℓ
 
 ------------------------------------------------------------------------
 -- Definition
@@ -56,28 +59,59 @@ transitive tr = trans tr tr
 asymmetric⇒empty : Asymmetric R → Empty (SymInterior R)
 asymmetric⇒empty asym (r , r′) = asym r r′
 
+-- Decidability
+decidable : Decidable R → Decidable (SymInterior R)
+does  (decidable R? x y) = does (R? x y) ∧ does (R? y x)
+proof (decidable R? x y) = proof (R? x y) reflects proof (R? y x)
+  where
+  _reflects_ : ∀ {bxy byx} → Reflects (R x y) bxy → Reflects (R y x) byx →
+               Reflects (SymInterior R x y) (bxy ∧ byx)
+  ofʸ rxy  reflects ofʸ ryx  = of (rxy , ryx)
+  ofʸ rxy  reflects ofⁿ ¬ryx = of (¬ryx ∘ rhs≤lhs)
+  ofⁿ ¬rxy reflects _        = of (¬rxy ∘ lhs≤rhs)
+
 -- A reflexive transitive relation _≤_ gives rise to a poset in which the
 -- equivalence relation is SymInterior _≤_.
 
-isEquivalence : Reflexive R → Transitive R → IsEquivalence (SymInterior R)
-isEquivalence refl trans = record
-  { refl = reflexive refl
-  ; sym = symmetric
-  ; trans = transitive trans
-  }
-
-isPartialOrder : Reflexive R → Transitive R → IsPartialOrder (SymInterior R) R
-isPartialOrder refl trans = record
-  { isPreorder = record
-    { isEquivalence = isEquivalence refl trans
+module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where
+
+  isEquivalence : IsEquivalence (SymInterior R)
+  isEquivalence = record
+    { refl = reflexive refl
+    ; sym = symmetric
+    ; trans = transitive trans
+    }
+
+  isPreorder : IsPreorder (SymInterior R) R
+  isPreorder = record
+    { isEquivalence = isEquivalence
     ; reflexive = lhs≤rhs
     ; trans = trans
     }
-  ; antisym = _,_
-  }
-
-poset : ∀ {a} {A : Set a} {R : Rel A ℓ} → Reflexive R → Transitive R → Poset a ℓ ℓ
-poset {R = R} refl trans = record
-  { _≤_ = R
-  ; isPartialOrder = isPartialOrder refl trans
-  }
+
+  isPartialOrder : IsPartialOrder (SymInterior R) R
+  isPartialOrder = record
+    { isPreorder = isPreorder
+    ; antisym = _,_
+    }
+
+  poset : Poset _ ℓ ℓ
+  poset = record { isPartialOrder = isPartialOrder }
+
+  module _ (R? : Decidable R) where
+
+    isDecEquivalence : IsDecEquivalence (SymInterior R)
+    isDecEquivalence = record
+      { isEquivalence = isEquivalence
+      ; _≟_ = decidable R?
+      }
+
+    isDecPartialOrder : IsDecPartialOrder (SymInterior R) R
+    isDecPartialOrder = record
+      { isPartialOrder = isPartialOrder
+      ; _≟_ = decidable R?
+      ; _≤?_ = R?
+      }
+
+    decPoset : DecPoset _ ℓ ℓ
+    decPoset = record { isDecPartialOrder = isDecPartialOrder }