diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5e52a3ae66..443c8de9b3 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
@@ -167,11 +174,6 @@ Additions to existing modules
   concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
   ```
 
-* In `Data.List.Relation.Unary.All`:
-  ```agda
-  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
-  ```
-
 * In `Data.List.Relation.Unary.Any.Properties`:
   ```agda
   concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
@@ -194,12 +196,60 @@ 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 ⊈ []
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/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/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."
+#-}