diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 76fa75cb2e..562e072f97 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -14,7 +14,9 @@ open import Data.Bool.Base
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.Product as Prod using (_×_; _,_)
 open import Data.These using (These; this; that; these)
+open import Function using (id; _∘_; _∘′_; flip)
 open import Function using (id; _∘_ ; _∘′_)
+
 open import Relation.Nullary using (yes; no)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Unary.Properties using (∁?)
@@ -286,8 +288,13 @@ break P? = span (∁? P?)
 ------------------------------------------------------------------------
 -- Operations for reversing lists
 
-reverse : ∀ {a} {A : Set a} → List A → List A
-reverse = foldl (λ rev x → x ∷ rev) []
+module _ {a} {A : Set a} where
+
+  reverseAcc : List A → List A → List A
+  reverseAcc = foldl (flip _∷_)
+
+  reverse : List A → List A
+  reverse = reverseAcc []
 
 -- Snoc.
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index ece05948fd..732441905f 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -637,17 +637,17 @@ module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where
 
 module _ {a} {A : Set a} where
 
-  unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
-  unfold-reverse x xs = helper [ x ] xs
-    where
-    open P.≡-Reasoning
-    helper : (xs ys : List A) → foldl (flip _∷_) xs ys ≡ reverse ys ++ xs
-    helper xs []       = refl
-    helper xs (y ∷ ys) = begin
-      foldl (flip _∷_) (y ∷ xs) ys  ≡⟨ helper (y ∷ xs) ys ⟩
-      reverse ys ++ y ∷ xs          ≡⟨ P.sym (++-assoc (reverse ys) _ _) ⟩
-      (reverse ys ∷ʳ y) ++ xs       ≡⟨ P.sym $ P.cong (_++ xs) (unfold-reverse y ys) ⟩
-      reverse (y ∷ ys) ++ xs        ∎
+  unfold-reverseAcc : (acc xs : List A) → reverseAcc acc xs ≡ reverse xs ++ acc
+  unfold-reverse    : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
+
+  unfold-reverse x xs = unfold-reverseAcc [ x ] xs
+
+  unfold-reverseAcc xs []       = refl
+  unfold-reverseAcc xs (y ∷ ys) = begin
+    foldl (flip _∷_) (y ∷ xs) ys  ≡⟨ unfold-reverseAcc (y ∷ xs) ys ⟩
+    reverse ys ++ y ∷ xs          ≡⟨ P.sym (++-assoc (reverse ys) _ _) ⟩
+    (reverse ys ∷ʳ y) ++ xs       ≡⟨ P.sym $ P.cong (_++ xs) (unfold-reverse y ys) ⟩
+    reverse (y ∷ ys) ++ xs        ∎ where open P.≡-Reasoning
 
   reverse-++-commute : (xs ys : List A) →
                        reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
diff --git a/src/Data/List/Relation/Equality/Setoid.agda b/src/Data/List/Relation/Equality/Setoid.agda
index f25320357d..7c56a2a3d3 100644
--- a/src/Data/List/Relation/Equality/Setoid.agda
+++ b/src/Data/List/Relation/Equality/Setoid.agda
@@ -55,4 +55,5 @@ open PW public using
   ; tabulate⁻
   ; ++⁺
   ; concat⁺
+  ; reverse⁺
   )
diff --git a/src/Data/List/Relation/Pointwise.agda b/src/Data/List/Relation/Pointwise.agda
index 6a454aa5f4..bd454206cc 100644
--- a/src/Data/List/Relation/Pointwise.agda
+++ b/src/Data/List/Relation/Pointwise.agda
@@ -10,6 +10,7 @@ open import Function
 open import Function.Inverse using (Inverse)
 open import Data.Product hiding (map)
 open import Data.List.Base hiding (map ; head ; tail)
+open import Data.List.Properties using (unfold-reverse)
 open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
 open import Data.Nat using (ℕ; zero; suc)
 open import Level
@@ -205,6 +206,21 @@ module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where
   concat⁺ []                = []
   concat⁺ (xs∼ys ∷ xss∼yss) = ++⁺ xs∼ys (concat⁺ xss∼yss)
 
+
+------------------------------------------------------------------------
+-- reverse
+
+module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where
+
+  reverseAcc⁺ : ∀ {xs ys us vs} → Pointwise _∼_ us vs → Pointwise _∼_ xs ys →
+                Pointwise _∼_ (reverseAcc us xs) (reverseAcc vs ys)
+  reverseAcc⁺ acc []            = acc
+  reverseAcc⁺ acc (x∼y ∷ xs∼ys) = reverseAcc⁺ (x∼y ∷ acc) xs∼ys
+
+  reverse⁺ : ∀ {xs ys} → Pointwise _∼_ xs ys →
+             Pointwise _∼_ (reverse xs) (reverse ys)
+  reverse⁺ = reverseAcc⁺ []
+
 ------------------------------------------------------------------------
 -- length
 
diff --git a/src/Data/List/Relation/Sublist/Inductive.agda b/src/Data/List/Relation/Sublist/Inductive.agda
deleted file mode 100644
index 15eea4b25d..0000000000
--- a/src/Data/List/Relation/Sublist/Inductive.agda
+++ /dev/null
@@ -1,48 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- An inductive definition of sublist. This is commonly known as an Order
--- Preserving Embedding (OPE).
-------------------------------------------------------------------------
-
-module Data.List.Relation.Sublist.Inductive where
-
-open import Data.List.Base using (List; []; _∷_; [_])
-open import Data.List.Any  using (here; there)
-open import Data.List.Membership.Propositional
-open import Relation.Binary using (Rel)
-open import Relation.Binary.PropositionalEquality using (refl)
-
-------------------------------------------------------------------------
--- Type and basic combinators
-
-module _ {a} {A : Set a} where
-
-  infix 3 _⊆_
-  data _⊆_ : Rel (List A) a where
-    base : [] ⊆ []
-    skip : ∀ {xs y ys} → xs ⊆ ys → xs ⊆ (y ∷ ys)
-    keep : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys)
-
-  infix 4 []⊆_
-  []⊆_ : ∀ xs → [] ⊆ xs
-  []⊆ []     = base
-  []⊆ x ∷ xs = skip ([]⊆ xs)
-
-------------------------------------------------------------------------
--- A function induced by a sublist proof
-
-  lookup : ∀ {xs ys} → xs ⊆ ys → {x : A} → x ∈ xs → x ∈ ys
-  lookup (skip p) v         = there (lookup p v)
-  lookup (keep p) (here px) = here px
-  lookup (keep p) (there v) = there (lookup p v)
-  lookup base     ()
-
--- Conversion between membership and proofs that a singleton is a sublist
-
-  from∈ : ∀ {xs x} → x ∈ xs → [ x ] ⊆ xs
-  from∈ (here refl) = keep ([]⊆ _)
-  from∈ (there p)   = skip (from∈ p)
-
-  to∈ : ∀ {xs x} → [ x ] ⊆ xs → x ∈ xs
-  to∈ p = lookup p (here refl)
diff --git a/src/Data/List/Relation/Sublist/Inductive/Properties.agda b/src/Data/List/Relation/Sublist/Inductive/Properties.agda
deleted file mode 100644
index ad617d1d37..0000000000
--- a/src/Data/List/Relation/Sublist/Inductive/Properties.agda
+++ /dev/null
@@ -1,360 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Sublist-related properties
-------------------------------------------------------------------------
-
-module Data.List.Relation.Sublist.Inductive.Properties where
-
-open import Data.Empty
-open import Data.List.Base hiding (lookup)
-open import Data.List.Properties
-open import Data.List.Any using (here; there)
-open import Data.List.Any.Properties using (here-injective; there-injective)
-open import Data.List.Membership.Propositional
-open import Data.List.Relation.Sublist.Inductive
-open import Data.Maybe as Maybe using (nothing; just)
-open import Data.Nat.Base
-open import Data.Nat.Properties
-
-open import Function
-import Function.Bijection as Bij
-open import Function.Equivalence as Equiv using (_⇔_ ; equivalence)
-import Function.Injection as Inj
-
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq hiding ([_])
-open import Relation.Nullary
-import Relation.Nullary.Decidable as D
-open import Relation.Unary as U using (Pred)
-
-------------------------------------------------------------------------
--- The `loookup` function induced by a proof that `xs ⊆ ys` is injective
-
-module _ {a} {A : Set a} where
-
-  lookup-injective : ∀ {x : A} {xs ys} {p : xs ⊆ ys} {v w : x ∈ xs} →
-                     lookup p v ≡ lookup p w → v ≡ w
-  lookup-injective {p = skip p} {v} {w} eq =
-    lookup-injective (there-injective eq)
-  lookup-injective {p = keep p} {here px} {here qx} eq =
-    cong here (≡-irrelevance _ _)
-  lookup-injective {p = keep p} {there v} {there w} eq =
-    cong there (lookup-injective (there-injective eq))
-  -- impossible cases
-  lookup-injective {p = keep p} {here px} {there w} ()
-  lookup-injective {p = keep p} {there v} {here qx} ()
-  lookup-injective {p = base} {}
-
-  []∈-irrelevant : U.Irrelevant {A = List A} ([] ⊆_)
-  []∈-irrelevant base     base     = refl
-  []∈-irrelevant (skip p) (skip q) = cong skip ([]∈-irrelevant p q)
-
-  [x]⊆xs↔x∈xs : ∀ {x : A} {xs} → ([ x ] ⊆ xs) Bij.⤖ (x ∈ xs)
-  [x]⊆xs↔x∈xs {x} = Bij.bijection to∈ from∈ (to∈-injective _ _) to∈∘from∈≗id
-
-    where
-
-    to∈-injective : ∀ {xs x} (p q : [ x ] ⊆ xs) → to∈ p ≡ to∈ q → p ≡ q
-    to∈-injective (skip p) (skip q) eq =
-      cong skip (to∈-injective p q (there-injective eq))
-    to∈-injective (keep p) (keep q) eq = cong keep ([]∈-irrelevant p q)
-    to∈-injective (skip p) (keep q) ()
-    to∈-injective (keep p) (skip q) ()
-
-    to∈∘from∈≗id : ∀ {xs} (p : x ∈ xs) → to∈ (from∈ p) ≡ p
-    to∈∘from∈≗id (here refl) = refl
-    to∈∘from∈≗id (there p)   = cong there (to∈∘from∈≗id p)
-
-------------------------------------------------------------------------
--- Some properties
-
-module _ {a} {A : Set a} where
-
-  ⊆-length : ∀ {xs ys : List A} → xs ⊆ ys → length xs ≤ length ys
-  ⊆-length base     = ≤-refl
-  ⊆-length (skip p) = ≤-step (⊆-length p)
-  ⊆-length (keep p) = s≤s (⊆-length p)
-
-------------------------------------------------------------------------
--- Relational properties
-
-module _ {a} {A : Set a} where
-
-  ⊆-reflexive : _≡_ ⇒ _⊆_ {A = A}
-  ⊆-reflexive {[]}     refl = base
-  ⊆-reflexive {x ∷ xs} refl = keep (⊆-reflexive refl)
-
-  ⊆-refl : Reflexive {A = List A} _⊆_
-  ⊆-refl = ⊆-reflexive refl
-
-  ⊆-trans : Transitive {A = List A} _⊆_
-  ⊆-trans p        base     = p
-  ⊆-trans p        (skip q) = skip (⊆-trans p q)
-  ⊆-trans (skip p) (keep q) = skip (⊆-trans p q)
-  ⊆-trans (keep p) (keep q) = keep (⊆-trans p q)
-
-  open ≤-Reasoning
-
-  ⊆-antisym : Antisymmetric {A = List A} _≡_ _⊆_
-  -- Positive cases
-  ⊆-antisym base     base     = refl
-  ⊆-antisym (keep p) (keep q) = cong (_ ∷_) (⊆-antisym p q)
-  -- Dismissing the impossible cases
-  ⊆-antisym {x ∷ xs} {y ∷ ys} (skip p) (skip q) = ⊥-elim $ 1+n≰n $ begin
-    length (y ∷ ys) ≤⟨ ⊆-length q ⟩
-    length xs       ≤⟨ n≤1+n (length xs) ⟩
-    length (x ∷ xs) ≤⟨ ⊆-length p ⟩
-    length ys       ∎
-  ⊆-antisym {x ∷ xs} {y ∷ ys} (skip p) (keep q) = ⊥-elim $ 1+n≰n $ begin
-    length (x ∷ xs) ≤⟨ ⊆-length p ⟩
-    length ys       ≤⟨ ⊆-length q ⟩
-    length xs       ∎
-  ⊆-antisym {x ∷ xs} {y ∷ ys} (keep p) (skip q) =  ⊥-elim $ 1+n≰n $ begin
-    length (y ∷ ys) ≤⟨ ⊆-length q ⟩
-    length xs       ≤⟨ ⊆-length p ⟩
-    length ys       ∎
-
-  ⊆-minimum : Minimum (_⊆_ {A = A}) []
-  ⊆-minimum = []⊆_
-
-module _ {a} (A : Set a) where
-
-  ⊆-isPreorder : IsPreorder _≡_ (_⊆_ {A = A})
-  ⊆-isPreorder = record
-    { isEquivalence = isEquivalence
-    ; reflexive     = ⊆-reflexive
-    ; trans         = ⊆-trans
-    }
-
-  ⊆-preorder : Preorder _ _ _
-  ⊆-preorder = record
-    { isPreorder = ⊆-isPreorder
-    }
-
-  ⊆-isPartialOrder : IsPartialOrder _≡_ _⊆_
-  ⊆-isPartialOrder = record
-    { isPreorder = ⊆-isPreorder
-    ; antisym    = ⊆-antisym
-    }
-
-  ⊆-poset : Poset _ _ _
-  ⊆-poset = record
-    { isPartialOrder = ⊆-isPartialOrder
-    }
-
-import Relation.Binary.PartialOrderReasoning as PosetReasoning
-module ⊆-Reasoning {a} {A : Set a}  where
-  private module P = PosetReasoning (⊆-poset A)
-  open P public
-    renaming (_≤⟨_⟩_ to _⊆⟨_⟩_; _≈⟨⟩_ to _≡⟨⟩_)
-    hiding (_≈⟨_⟩_)
-
-
-------------------------------------------------------------------------
--- Various functions' outputs are sublists
-
-module _ {a} {A : Set a} where
-
-  tail-⊆ : (xs : List A) → Maybe.All (_⊆ xs) (tail xs)
-  tail-⊆ []       = nothing
-  tail-⊆ (x ∷ xs) = just (skip ⊆-refl)
-
-  take-⊆ : ∀ n (xs : List A) → take n xs ⊆ xs
-  take-⊆ zero    xs       = []⊆ xs
-  take-⊆ (suc n) []       = []⊆ []
-  take-⊆ (suc n) (x ∷ xs) = keep (take-⊆ n xs)
-
-  drop-⊆ : ∀ n (xs : List A) → drop n xs ⊆ xs
-  drop-⊆ zero    xs       = ⊆-refl
-  drop-⊆ (suc n) []       = []⊆ []
-  drop-⊆ (suc n) (x ∷ xs) = skip (drop-⊆ n xs)
-
-module _ {a p} {A : Set a} {P : Pred A p} (P? : U.Decidable P) where
-
-  takeWhile-⊆ : ∀ xs → takeWhile P? xs ⊆ xs
-  takeWhile-⊆ []       = []⊆ []
-  takeWhile-⊆ (x ∷ xs) with P? x
-  ... | yes p = keep (takeWhile-⊆ xs)
-  ... | no ¬p = []⊆ x ∷ xs
-
-  dropWhile-⊆ : ∀ xs → dropWhile P? xs ⊆ xs
-  dropWhile-⊆ []       = []⊆ []
-  dropWhile-⊆ (x ∷ xs) with P? x
-  ... | yes p = skip (dropWhile-⊆ xs)
-  ... | no ¬p = ⊆-refl
-
-  filter-⊆ : ∀ xs → filter P? xs ⊆ xs
-  filter-⊆ []       = []⊆ []
-  filter-⊆ (x ∷ xs) with P? x
-  ... | yes p = keep (filter-⊆ xs)
-  ... | no ¬p = skip (filter-⊆ xs)
-
-------------------------------------------------------------------------
--- Various functions are increasing wrt _⊆_
-
-
-------------------------------------------------------------------------
--- _∷_
-
-module _ {a} {A : Set a} where
-
-  ∷⁻ : ∀ x {us vs : List A} → x ∷ us ⊆ x ∷ vs → us ⊆ vs
-  ∷⁻ x (skip p) = ⊆-trans (skip ⊆-refl) p
-  ∷⁻ x (keep p) = p
-
--- map
-
-module _ {a b} {A : Set a} {B : Set b} where
-
-  map⁺ : ∀ {xs ys} (f : A → B) → xs ⊆ ys → map f xs ⊆ map f ys
-  map⁺ f base     = base
-  map⁺ f (skip p) = skip (map⁺ f p)
-  map⁺ f (keep p) = keep (map⁺ f p)
-
-  open Inj.Injection
-
-  map⁻ : ∀ {xs ys} (inj : A Inj.↣ B) →
-         map (inj ⟨$⟩_) xs ⊆ map (inj ⟨$⟩_) ys → xs ⊆ ys
-  map⁻ {[]}     {ys}     inj p = []⊆ ys
-  map⁻ {x ∷ xs} {[]}     inj ()
-  map⁻ {x ∷ xs} {y ∷ ys} inj p
-    with inj ⟨$⟩ x | inspect (inj ⟨$⟩_) x
-       | inj ⟨$⟩ y | inspect (inj ⟨$⟩_) y
-       | injective inj {x} {y}
-  map⁻ {x ∷ xs} {y ∷ ys} inj (skip p)
-    | fx | Eq.[ eq ] | fy | _ | _ = skip (map⁻ inj (coerce p))
-    where coerce = subst (λ fx → fx ∷ _ ⊆ _) (sym eq)
-  map⁻ {x ∷ xs} {y ∷ ys} inj (keep p)
-    | fx | _      | fx | _ | eq
-    rewrite eq refl = keep (map⁻ inj p)
-
--- _++_
-
-module _ {a} {A : Set a} where
-
-  ++⁺ : ∀ {xs ys us vs : List A} → xs ⊆ ys → us ⊆ vs → xs ++ us ⊆ ys ++ vs
-  ++⁺ base     q = q
-  ++⁺ (skip p) q = skip (++⁺ p q)
-  ++⁺ (keep p) q = keep (++⁺ p q)
-
-  ++⁻ : ∀ xs {us vs : List A} → xs ++ us ⊆ xs ++ vs → us ⊆ vs
-  ++⁻ []       p = p
-  ++⁻ (x ∷ xs) p = ++⁻ xs (∷⁻ x p)
-
-  skips : ∀ {xs ys} (zs : List A) → xs ⊆ ys → xs ⊆ zs ++ ys
-  skips zs = ++⁺ ([]⊆ zs)
-
--- take / drop
-
-  ≤-take-⊆ : ∀ {m n} → m ≤ n → (xs : List A) → take m xs ⊆ take n xs
-  ≤-take-⊆ z≤n     xs       = []⊆ take _ xs
-  ≤-take-⊆ (s≤s p) []       = []⊆ []
-  ≤-take-⊆ (s≤s p) (x ∷ xs) = keep (≤-take-⊆ p xs)
-
-  ≥-drop-⊆ : ∀ {m n} → m ≥ n → (xs : List A) → drop m xs ⊆ drop n xs
-  ≥-drop-⊆ {m} z≤n     xs       = drop-⊆ m xs
-  ≥-drop-⊆     (s≤s p) []       = []⊆ []
-  ≥-drop-⊆     (s≤s p) (x ∷ xs) = ≥-drop-⊆ p xs
-
-  drop⁺ : ∀ n {xs ys : List A} → xs ⊆ ys → drop n xs ⊆ drop n ys
-  drop⁺ zero    p        = p
-  drop⁺ (suc n) base     = []⊆ []
-  drop⁺ (suc n) (keep p) = drop⁺ n p
-  drop⁺ (suc n) {xs} {y ∷ ys} (skip p) = begin
-    drop (suc n) xs ⊆⟨ ≥-drop-⊆ (n≤1+n n) xs ⟩
-    drop n xs       ⊆⟨ drop⁺ n p ⟩
-    drop n ys       ∎ where open ⊆-Reasoning
-
-module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q}
-         (P? : U.Decidable P) (Q? : U.Decidable Q) where
-
-  ⊆-takeWhile-⊆ : (P U.⊆ Q) → ∀ xs → takeWhile P? xs ⊆ takeWhile Q? xs
-  ⊆-takeWhile-⊆ P⊆Q []       = []⊆ []
-  ⊆-takeWhile-⊆ P⊆Q (x ∷ xs) with P? x | Q? x
-  ... | yes px | yes qx = keep (⊆-takeWhile-⊆ P⊆Q xs)
-  ... | yes px | no ¬qx = ⊥-elim $ ¬qx (P⊆Q px)
-  ... | no ¬px | _      = []⊆ _
-
-  ⊇-dropWhile-⊆ : (P U.⊇ Q) → ∀ xs → dropWhile P? xs ⊆ dropWhile Q? xs
-  ⊇-dropWhile-⊆ P⊇Q []       = []⊆ []
-  ⊇-dropWhile-⊆ P⊇Q (x ∷ xs) with P? x | Q? x
-  ... | yes px | yes qx = ⊇-dropWhile-⊆ P⊇Q xs
-  ... | yes px | no ¬qx = skip (dropWhile-⊆ P? xs)
-  ... | no ¬px | yes qx = ⊥-elim $ ¬px (P⊇Q qx)
-  ... | no ¬px | no ¬qx = ⊆-refl
-
--- filter
-
-  ⊆-filter-⊆ : (P U.⊆ Q) → ∀ xs → filter P? xs ⊆ filter Q? xs
-  ⊆-filter-⊆ P⊆Q []       = []⊆ []
-  ⊆-filter-⊆ P⊆Q (x ∷ xs) with P? x | Q? x
-  ... | yes px | yes qx = keep (⊆-filter-⊆ P⊆Q xs)
-  ... | yes px | no ¬qx = ⊥-elim $ ¬qx (P⊆Q px)
-  ... | no ¬px | yes qx = skip (⊆-filter-⊆ P⊆Q xs)
-  ... | no ¬px | no ¬qx = ⊆-filter-⊆ P⊆Q xs
-
-module _ {a p} {A : Set a} {P : Pred A p} (P? : U.Decidable P) where
-
-  filter⁺ : ∀ {xs ys : List A} → xs ⊆ ys → filter P? xs ⊆ filter P? ys
-  filter⁺                   base     = base
-  filter⁺ {xs}     {y ∷ ys} (skip p) with P? y
-  ... | yes py = skip (filter⁺ p)
-  ... | no ¬py = filter⁺ p
-  filter⁺ {x ∷ xs} {x ∷ ys} (keep p) with P? x
-  ... | yes px = keep (filter⁺ p)
-  ... | no ¬px = filter⁺ p
-
--- reverse
-
-module _ {a} {A : Set a} where
-
-  open ⊆-Reasoning
-
-  reverse⁺ : {xs ys : List A} → xs ⊆ ys → reverse xs ⊆ reverse ys
-  reverse⁺ base = []⊆ []
-  reverse⁺ {xs} {y ∷ ys} (skip p) = begin
-    reverse xs       ≡⟨ sym $ ++-identityʳ _ ⟩
-    reverse xs ++ [] ⊆⟨ ++⁺ (reverse⁺ p) ([]⊆ _) ⟩
-    reverse ys ∷ʳ y  ≡⟨ sym $ unfold-reverse y ys ⟩
-    reverse (y ∷ ys) ∎
-  reverse⁺ {x ∷ xs} {x ∷ ys} (keep p) = begin
-    reverse (x ∷ xs) ≡⟨ unfold-reverse x xs ⟩
-    reverse xs ∷ʳ x  ⊆⟨ ++⁺ (reverse⁺ p) ⊆-refl ⟩
-    reverse ys ∷ʳ x  ≡⟨ sym $ unfold-reverse x ys ⟩
-    reverse (x ∷ ys) ∎
-
-  reverse⁻ : {xs ys : List A} → reverse xs ⊆ reverse ys → xs ⊆ ys
-  reverse⁻ {xs} {ys} p = cast (reverse⁺ p) where
-    cast = subst₂ _⊆_ (reverse-involutive xs) (reverse-involutive ys)
-
-
-------------------------------------------------------------------------
--- Inversion lemmas
-
-module _ {a} {A : Set a} where
-
-  keep⁻¹ : ∀ (x : A) {xs ys} → (xs ⊆ ys) ⇔ (x ∷ xs ⊆ x ∷ ys)
-  keep⁻¹ x = equivalence keep (∷⁻ x)
-
-  skip⁻¹ : ∀ {x y : A} {xs ys} → x ≢ y → (x ∷ xs ⊆ ys) ⇔ (x ∷ xs ⊆ y ∷ ys)
-  skip⁻¹ ¬eq = equivalence skip $ λ where
-    (skip p) → p
-    (keep p) → ⊥-elim (¬eq refl)
-
-  ++⁻¹ : ∀ (ps : List A) {xs ys} → (xs ⊆ ys) ⇔ (ps ++ xs ⊆ ps ++ ys)
-  ++⁻¹ ps = equivalence (++⁺ ⊆-refl) (++⁻ ps)
-
-------------------------------------------------------------------------
--- Decidability of the order
-
-module Decidable
-       {a} {A : Set a} (eq? : Decidable {A = A} _≡_) where
-
-  infix 3 _⊆?_
-  _⊆?_ : Decidable {A = List A} _⊆_
-  []     ⊆? ys     = yes ([]⊆ ys)
-  x ∷ xs ⊆? []     = no λ ()
-  x ∷ xs ⊆? y ∷ ys with eq? x y
-  ... | yes refl = D.map (keep⁻¹ x) (xs ⊆? ys)
-  ... | no ¬eq   = D.map (skip⁻¹ ¬eq) (x ∷ xs ⊆? ys)
diff --git a/src/Data/List/Relation/Sublist/Inductive/Propositional.agda b/src/Data/List/Relation/Sublist/Inductive/Propositional.agda
new file mode 100644
index 0000000000..dc3660e6f8
--- /dev/null
+++ b/src/Data/List/Relation/Sublist/Inductive/Propositional.agda
@@ -0,0 +1,13 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Propositional version of the sublist relation. This is commonly known
+-- as an Order Preserving Embedding (OPE).
+------------------------------------------------------------------------
+
+module Data.List.Relation.Sublist.Inductive.Propositional where
+
+open import Relation.Binary.PropositionalEquality
+import Data.List.Relation.Sublist.Inductive.Setoid as Sublist
+
+open module S {a} {A : Set a} = Sublist (setoid A) public
diff --git a/src/Data/List/Relation/Sublist/Inductive/Propositional/Properties.agda b/src/Data/List/Relation/Sublist/Inductive/Propositional/Properties.agda
new file mode 100644
index 0000000000..4993acd037
--- /dev/null
+++ b/src/Data/List/Relation/Sublist/Inductive/Propositional/Properties.agda
@@ -0,0 +1,83 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Propositional sublist-related properties
+------------------------------------------------------------------------
+
+module Data.List.Relation.Sublist.Inductive.Propositional.Properties where
+
+import Data.List.Base as List
+open import Data.List.Any using (here; there)
+open import Data.List.Any.Properties using (here-injective; there-injective)
+open import Data.List.Membership.Propositional
+import Data.List.Relation.Sublist.Inductive.Setoid as Sublist
+import Data.List.Relation.Sublist.Inductive.Setoid.Properties as SublistProp
+import Function.Injection as Inj
+import Function.Bijection as Bij
+open import Relation.Binary.PropositionalEquality
+
+private open module S {a} {A : Set a} = Sublist (setoid A)
+
+-- We re-exports all the properties obtained for setoids except for the ones which
+-- can be specialized further.
+
+open module SProp {a} {A : Set a} = SublistProp (setoid A)
+  hiding (map⁺; map⁻)
+  public
+
+-- We provide specialized versions of the properties we can simplify
+
+module _ {a b} {A : Set a} {B : Set b} where
+
+  map⁺ : ∀ {xs ys} (f : A → B) → xs ⊆ ys → List.map f xs ⊆ List.map f ys
+  map⁺ f = SProp.map⁺ (setoid _) (cong f)
+
+  open Inj.Injection
+
+  map⁻ : ∀ {xs ys} (inj : A Inj.↣ B) →
+         List.map (inj ⟨$⟩_) xs ⊆ List.map (inj ⟨$⟩_) ys → xs ⊆ ys
+  map⁻ = SProp.map⁻ (setoid _)
+
+-- We provide additional properties we can't handle (yet) in the general
+-- setoid case
+
+
+------------------------------------------------------------------------
+-- The `loookup` function induced by a proof that `xs ⊆ ys` is injective
+
+module _ {a} {A : Set a} where
+
+  lookup-injective : ∀ {x : A} {xs ys} {p : xs ⊆ ys} {v w : x ∈ xs} →
+                     lookup p v ≡ lookup p w → v ≡ w
+  lookup-injective {p = skip p} {v} {w} eq =
+    lookup-injective (there-injective eq)
+  lookup-injective {p = keep refl p} {here px} {here qx} eq =
+    cong here (≡-irrelevance _ _)
+  lookup-injective {p = keep refl p} {there v} {there w} eq =
+    cong there (lookup-injective (there-injective eq))
+  -- impossible cases
+  lookup-injective {p = keep refl p} {here px} {there w} ()
+  lookup-injective {p = keep refl p} {there v} {here qx} ()
+  lookup-injective {p = base} {}
+
+------------------------------------------------------------------------
+-- The singleton list being a sublist of xs is isomorphic to its element
+-- belonging to xs.
+
+  [x]⊆xs↔x∈xs : ∀ {x : A} {xs} → (List.[ x ] ⊆ xs) Bij.⤖ (x ∈ xs)
+  [x]⊆xs↔x∈xs {x} = Bij.bijection to∈ from∈ (to∈-injective _ _) to∈∘from∈≗id
+
+    where
+
+    to∈-injective : ∀ {xs x} (p q : List.[ x ] ⊆ xs) → to∈ p ≡ to∈ q → p ≡ q
+    to∈-injective (skip p) (skip q) eq =
+      cong skip (to∈-injective p q (there-injective eq))
+    to∈-injective (keep eq₁ p) (keep eq₂ q) eq =
+      cong₂ keep (≡-irrelevance eq₁ eq₂) ([]⊆-irrelevant p q)
+    to∈-injective (skip p) (keep eq q) ()
+    to∈-injective (keep eq p) (skip q) ()
+
+    to∈∘from∈≗id : ∀ {xs} (p : x ∈ xs) → to∈ (from∈ p) ≡ p
+    to∈∘from∈≗id (here refl) = refl
+    to∈∘from∈≗id (there p)   = cong there (to∈∘from∈≗id p)
+
diff --git a/src/Data/List/Relation/Sublist/Inductive/Propositional/Solver.agda b/src/Data/List/Relation/Sublist/Inductive/Propositional/Solver.agda
new file mode 100644
index 0000000000..672c3fcf4e
--- /dev/null
+++ b/src/Data/List/Relation/Sublist/Inductive/Propositional/Solver.agda
@@ -0,0 +1,11 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for proving that one list is a sublist of the other.
+------------------------------------------------------------------------
+
+module Data.List.Relation.Sublist.Inductive.Propositional.Solver where
+
+open import Relation.Binary.PropositionalEquality
+import Data.List.Relation.Sublist.Inductive.Setoid.Solver as SubSolver
+open module S {a} {A : Set a} = SubSolver (setoid A) public
diff --git a/src/Data/List/Relation/Sublist/Inductive/Setoid.agda b/src/Data/List/Relation/Sublist/Inductive/Setoid.agda
new file mode 100644
index 0000000000..6425328aa7
--- /dev/null
+++ b/src/Data/List/Relation/Sublist/Inductive/Setoid.agda
@@ -0,0 +1,49 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An inductive definition of sublist. This is commonly known as an Order
+-- Preserving Embedding (OPE).
+------------------------------------------------------------------------
+
+open import Relation.Binary using (Rel; Setoid)
+
+module Data.List.Relation.Sublist.Inductive.Setoid
+       {c ℓ} (S : Setoid c ℓ) where
+
+open import Data.List.Base using (List; []; _∷_; [_])
+open import Data.List.Any  using (here; there)
+open import Data.List.Membership.Setoid S
+
+open Setoid S renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Type and basic combinators
+
+infix 3 _⊆_
+data _⊆_ : Rel (List A) ℓ where
+  base : [] ⊆ []
+  skip : ∀ {xs y ys} → xs ⊆ ys → xs ⊆ (y ∷ ys)
+  keep : ∀ {x y xs ys} → x ≈ y → xs ⊆ ys → (x ∷ xs) ⊆ (y ∷ ys)
+
+infix 4 []⊆_
+[]⊆_ : ∀ xs → [] ⊆ xs
+[]⊆ []     = base
+[]⊆ x ∷ xs = skip ([]⊆ xs)
+
+------------------------------------------------------------------------
+-- A function induced by a sublist proof
+
+lookup : ∀ {xs ys} → xs ⊆ ys → {x : A} → x ∈ xs → x ∈ ys
+lookup (skip p)     v          = there (lookup p v)
+lookup (keep x≈y p) (here z≈x) = here (trans z≈x x≈y)
+lookup (keep x≈y p) (there v)  = there (lookup p v)
+lookup base         ()
+
+-- Conversion between membership and proofs that a singleton is a sublist
+
+from∈ : ∀ {xs x} → x ∈ xs → [ x ] ⊆ xs
+from∈ (here x≈y) = keep x≈y ([]⊆ _)
+from∈ (there p)  = skip (from∈ p)
+
+to∈ : ∀ {xs x} → [ x ] ⊆ xs → x ∈ xs
+to∈ p = lookup p (here refl)
diff --git a/src/Data/List/Relation/Sublist/Inductive/Setoid/Properties.agda b/src/Data/List/Relation/Sublist/Inductive/Setoid/Properties.agda
new file mode 100644
index 0000000000..37ef403fc9
--- /dev/null
+++ b/src/Data/List/Relation/Sublist/Inductive/Setoid/Properties.agda
@@ -0,0 +1,319 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Sublist-related properties
+------------------------------------------------------------------------
+
+open import Relation.Binary
+
+module Data.List.Relation.Sublist.Inductive.Setoid.Properties
+       {c ℓ} (S : Setoid c ℓ) where
+
+open import Data.Empty
+open import Data.List.Base hiding (lookup)
+open import Data.List.Properties
+open import Data.List.Any using (here; there)
+open import Data.List.Any.Properties using (here-injective; there-injective)
+open import Data.Maybe as Maybe using (nothing; just)
+open import Data.Nat.Base
+open import Data.Nat.Properties
+
+open import Data.List.Membership.Setoid S
+open import Data.List.Relation.Equality.Setoid S as Eq
+  using (_≋_; []; _∷_; ≋-refl; ≋-isEquivalence)
+import Data.List.Relation.Sublist.Inductive.Setoid as Sublist
+open Sublist S
+
+
+open import Function
+import Function.Bijection as Bij
+open import Function.Equivalence as Equiv using (_⇔_ ; equivalence)
+import Function.Injection as Inj
+
+import Algebra.FunctionProperties as FunProp
+
+open import Relation.Nullary
+import Relation.Nullary.Decidable as D
+open import Relation.Unary as U using (Pred)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+private module S = Setoid S renaming (Carrier to A)
+open S
+
+------------------------------------------------------------------------
+-- []⊆_ is irrelevant.
+
+[]⊆-irrelevant : U.Irrelevant ([] ⊆_)
+[]⊆-irrelevant base     base     = P.refl
+[]⊆-irrelevant (skip p) (skip q) = P.cong skip ([]⊆-irrelevant p q)
+
+
+------------------------------------------------------------------------
+-- Some properties
+
+⊆-length : ∀ {xs ys} → xs ⊆ ys → length xs ≤ length ys
+⊆-length base         = ≤-refl
+⊆-length (skip p)     = ≤-step (⊆-length p)
+⊆-length (keep x≈y p) = s≤s (⊆-length p)
+
+------------------------------------------------------------------------
+-- Relational properties
+
+⊆-reflexive : _≋_ ⇒ _⊆_
+⊆-reflexive []            = base
+⊆-reflexive (x≈y ∷ xs≈ys) = keep x≈y (⊆-reflexive xs≈ys)
+
+⊆-refl : Reflexive _⊆_
+⊆-refl = ⊆-reflexive ≋-refl
+
+⊆-trans : Transitive _⊆_
+⊆-trans p            base         = p
+⊆-trans p            (skip q)     = skip (⊆-trans p q)
+⊆-trans (skip p)     (keep x≈y q) = skip (⊆-trans p q)
+⊆-trans (keep x≈y p) (keep y≈z q) = keep (trans x≈y y≈z) (⊆-trans p q)
+
+
+⊆-antisym : Antisymmetric _≋_ _⊆_
+-- Positive cases
+⊆-antisym base         base         = []
+⊆-antisym (keep x≈y p) (keep y≈x q) = x≈y ∷ ⊆-antisym p q
+-- Dismissing the impossible cases
+⊆-antisym {x ∷ xs} {y ∷ ys} (skip p) (skip q) = ⊥-elim $ 1+n≰n $ begin
+  length (y ∷ ys) ≤⟨ ⊆-length q ⟩
+  length xs       ≤⟨ n≤1+n (length xs) ⟩
+  length (x ∷ xs) ≤⟨ ⊆-length p ⟩
+  length ys       ∎ where open ≤-Reasoning
+⊆-antisym {x ∷ xs} {y ∷ ys} (skip p) (keep x≈y q) = ⊥-elim $ 1+n≰n $ begin
+  length (x ∷ xs) ≤⟨ ⊆-length p ⟩
+  length ys       ≤⟨ ⊆-length q ⟩
+  length xs       ∎ where open ≤-Reasoning
+⊆-antisym {x ∷ xs} {y ∷ ys} (keep x≈y p) (skip q) =  ⊥-elim $ 1+n≰n $ begin
+  length (y ∷ ys) ≤⟨ ⊆-length q ⟩
+  length xs       ≤⟨ ⊆-length p ⟩
+  length ys       ∎ where open ≤-Reasoning
+
+⊆-minimum : Minimum _⊆_ []
+⊆-minimum = []⊆_
+
+
+⊆-isPreorder : IsPreorder _≋_ _⊆_
+⊆-isPreorder = record
+  { isEquivalence = ≋-isEquivalence
+  ; reflexive     = ⊆-reflexive
+  ; trans         = ⊆-trans
+  }
+
+⊆-preorder : Preorder _ _ _
+⊆-preorder = record
+  { isPreorder = ⊆-isPreorder
+  }
+
+⊆-isPartialOrder : IsPartialOrder _≋_ _⊆_
+⊆-isPartialOrder = record
+  { isPreorder = ⊆-isPreorder
+  ; antisym    = ⊆-antisym
+  }
+
+⊆-poset : Poset _ _ _
+⊆-poset = record
+  { isPartialOrder = ⊆-isPartialOrder
+  }
+
+import Relation.Binary.PartialOrderReasoning as PosetReasoning
+module ⊆-Reasoning where
+  private module PR = PosetReasoning ⊆-poset
+  open PR public renaming (_≤⟨_⟩_ to _⊆⟨_⟩_; _≈⟨_⟩_ to _≋⟨_⟩_)
+
+------------------------------------------------------------------------
+-- Various functions' outputs are sublists
+
+tail-⊆ : ∀ xs → Maybe.All (_⊆ xs) (tail xs)
+tail-⊆ []       = nothing
+tail-⊆ (x ∷ xs) = just (skip ⊆-refl)
+
+take-⊆ : ∀ n xs → take n xs ⊆ xs
+take-⊆ zero    xs       = []⊆ xs
+take-⊆ (suc n) []       = []⊆ []
+take-⊆ (suc n) (x ∷ xs) = keep refl (take-⊆ n xs)
+
+drop-⊆ : ∀ n xs → drop n xs ⊆ xs
+drop-⊆ zero    xs       = ⊆-refl
+drop-⊆ (suc n) []       = []⊆ []
+drop-⊆ (suc n) (x ∷ xs) = skip (drop-⊆ n xs)
+
+module _ {p} {P : Pred A p} (P? : U.Decidable P) where
+
+  takeWhile-⊆ : ∀ xs → takeWhile P? xs ⊆ xs
+  takeWhile-⊆ []       = []⊆ []
+  takeWhile-⊆ (x ∷ xs) with P? x
+  ... | yes p = keep refl (takeWhile-⊆ xs)
+  ... | no ¬p = []⊆ x ∷ xs
+
+  dropWhile-⊆ : ∀ xs → dropWhile P? xs ⊆ xs
+  dropWhile-⊆ []       = []⊆ []
+  dropWhile-⊆ (x ∷ xs) with P? x
+  ... | yes p = skip (dropWhile-⊆ xs)
+  ... | no ¬p = ⊆-refl
+
+  filter-⊆ : ∀ xs → filter P? xs ⊆ xs
+  filter-⊆ []       = []⊆ []
+  filter-⊆ (x ∷ xs) with P? x
+  ... | yes p = keep refl (filter-⊆ xs)
+  ... | no ¬p = skip (filter-⊆ xs)
+
+------------------------------------------------------------------------
+-- Various functions are increasing wrt _⊆_
+
+
+------------------------------------------------------------------------
+-- _∷_
+
+∷⁻ : ∀ {x y xs ys} → x ≈ y → x ∷ xs ⊆ y ∷ ys → xs ⊆ ys
+∷⁻ x≈y (skip p)      = ⊆-trans (skip ⊆-refl) p
+∷⁻ x≈y (keep x≈y′ p) = p
+
+-- map
+
+module _ {d ℓ′} (T : Setoid d ℓ′) where
+
+  open Setoid T renaming (Carrier to B; _≈_ to _≈′_)
+  module T = Sublist T
+
+  map⁺ : ∀ {f xs ys} → f Preserves _≈_ ⟶ _≈′_ →
+         xs ⊆ ys → map f xs T.⊆ map f ys
+  map⁺ f base         = T.base
+  map⁺ f (skip p)     = T.skip (map⁺ f p)
+  map⁺ f (keep x≈y p) = T.keep (f x≈y) (map⁺ f p)
+
+  open Inj.Injection
+
+  map⁻ : ∀ {xs ys} (inj : Inj.Injection S T) →
+         map (inj ⟨$⟩_) xs T.⊆ map (inj ⟨$⟩_) ys → xs ⊆ ys
+  map⁻ {[]}     {ys}     inj p = []⊆ ys
+  map⁻ {x ∷ xs} {[]}     inj ()
+  map⁻ {x ∷ xs} {y ∷ ys} inj p
+    with inj ⟨$⟩ x | P.inspect (inj ⟨$⟩_) x
+       | inj ⟨$⟩ y | P.inspect (inj ⟨$⟩_) y
+       | injective inj {x} {y}
+  map⁻ {x ∷ xs} {y ∷ ys} inj (skip p)
+    | fx | P.[ eq ] | fy | _ | _ = skip (map⁻ inj (coerce p))
+    where coerce = P.subst (λ fx → fx ∷ _ T.⊆ _) (P.sym eq)
+  map⁻ {x ∷ xs} {y ∷ ys} inj (keep x≈y p)
+    | fx | _      | fy | _ | eq = keep (eq x≈y) (map⁻ inj p)
+
+-- _++_
+
+++⁺ : ∀ {xs ys us vs} → xs ⊆ ys → us ⊆ vs → xs ++ us ⊆ ys ++ vs
+++⁺ base         q = q
+++⁺ (skip p)     q = skip (++⁺ p q)
+++⁺ (keep x≈y p) q = keep x≈y (++⁺ p q)
+
+++⁻ : ∀ xs {us vs} → xs ++ us ⊆ xs ++ vs → us ⊆ vs
+++⁻ []       p = p
+++⁻ (x ∷ xs) p = ++⁻ xs (∷⁻ refl p)
+
+skips : ∀ {xs ys} zs → xs ⊆ ys → xs ⊆ zs ++ ys
+skips zs = ++⁺ ([]⊆ zs)
+
+-- take / drop
+
+≤-take-⊆ : ∀ {m n} → m ≤ n → ∀ xs → take m xs ⊆ take n xs
+≤-take-⊆ z≤n     xs       = []⊆ take _ xs
+≤-take-⊆ (s≤s p) []       = []⊆ []
+≤-take-⊆ (s≤s p) (x ∷ xs) = keep refl (≤-take-⊆ p xs)
+
+≥-drop-⊆ : ∀ {m n} → m ≥ n → ∀ xs → drop m xs ⊆ drop n xs
+≥-drop-⊆ {m} z≤n     xs       = drop-⊆ m xs
+≥-drop-⊆     (s≤s p) []       = []⊆ []
+≥-drop-⊆     (s≤s p) (x ∷ xs) = ≥-drop-⊆ p xs
+
+drop⁺ : ∀ n {xs ys : List A} → xs ⊆ ys → drop n xs ⊆ drop n ys
+drop⁺ zero    p            = p
+drop⁺ (suc n) base         = []⊆ []
+drop⁺ (suc n) (keep x≈y p) = drop⁺ n p
+drop⁺ (suc n) {xs} {y ∷ ys} (skip p) = begin
+  drop (suc n) xs ⊆⟨ ≥-drop-⊆ (n≤1+n n) xs ⟩
+  drop n xs       ⊆⟨ drop⁺ n p ⟩
+  drop n ys       ∎ where open ⊆-Reasoning
+
+module _ {p q} {P : Pred A p} {Q : Pred A q}
+         (P? : U.Decidable P) (Q? : U.Decidable Q) where
+
+  ⊆-takeWhile-⊆ : (P U.⊆ Q) → ∀ xs → takeWhile P? xs ⊆ takeWhile Q? xs
+  ⊆-takeWhile-⊆ P⊆Q []       = []⊆ []
+  ⊆-takeWhile-⊆ P⊆Q (x ∷ xs) with P? x | Q? x
+  ... | yes px | yes qx = keep refl (⊆-takeWhile-⊆ P⊆Q xs)
+  ... | yes px | no ¬qx = ⊥-elim $ ¬qx (P⊆Q px)
+  ... | no ¬px | _      = []⊆ _
+
+  ⊇-dropWhile-⊆ : (P U.⊇ Q) → ∀ xs → dropWhile P? xs ⊆ dropWhile Q? xs
+  ⊇-dropWhile-⊆ P⊇Q []       = []⊆ []
+  ⊇-dropWhile-⊆ P⊇Q (x ∷ xs) with P? x | Q? x
+  ... | yes px | yes qx = ⊇-dropWhile-⊆ P⊇Q xs
+  ... | yes px | no ¬qx = skip (dropWhile-⊆ P? xs)
+  ... | no ¬px | yes qx = ⊥-elim $ ¬px (P⊇Q qx)
+  ... | no ¬px | no ¬qx = ⊆-refl
+
+-- filter
+
+  ⊆-filter-⊆ : (P U.⊆ Q) → ∀ xs → filter P? xs ⊆ filter Q? xs
+  ⊆-filter-⊆ P⊆Q []       = []⊆ []
+  ⊆-filter-⊆ P⊆Q (x ∷ xs) with P? x | Q? x
+  ... | yes px | yes qx = keep refl (⊆-filter-⊆ P⊆Q xs)
+  ... | yes px | no ¬qx = ⊥-elim $ ¬qx (P⊆Q px)
+  ... | no ¬px | yes qx = skip (⊆-filter-⊆ P⊆Q xs)
+  ... | no ¬px | no ¬qx = ⊆-filter-⊆ P⊆Q xs
+
+module _ {p} {P : Pred A p} (P? : U.Decidable P) (P≈ : P Respects _≈_) where
+
+  filter⁺ : ∀ {xs ys} → xs ⊆ ys → filter P? xs ⊆ filter P? ys
+  filter⁺                   base     = base
+  filter⁺ {xs}     {y ∷ ys} (skip p) with P? y
+  ... | yes py = skip (filter⁺ p)
+  ... | no ¬py = filter⁺ p
+  filter⁺ {x ∷ xs} {y ∷ ys} (keep x≈y p) with P? x | P? y
+  ... | yes px | yes py = keep x≈y (filter⁺ p)
+  ... | no ¬px | no ¬py = filter⁺ p
+  ... | yes px | no ¬py = ⊥-elim $ ¬py (P≈ x≈y px)
+  ... | no ¬px | yes py = ⊥-elim $ ¬px (P≈ (sym x≈y) py)
+
+-- reverse
+
+reverseAcc⁺ : ∀ {us vs xs ys} → us ⊆ vs → xs ⊆ ys → reverseAcc us xs ⊆ reverseAcc vs ys
+reverseAcc⁺ acc base         = acc
+reverseAcc⁺ acc (skip p)     = reverseAcc⁺ (skip acc) p
+reverseAcc⁺ acc (keep x≈y p) = reverseAcc⁺ (keep x≈y acc) p
+
+reverse⁺ : ∀ {xs ys} → xs ⊆ ys → reverse xs ⊆ reverse ys
+reverse⁺ = reverseAcc⁺ base
+
+reverse⁻ : ∀ {xs ys} → reverse xs ⊆ reverse ys → xs ⊆ ys
+reverse⁻ {xs} {ys} p = cast (reverse⁺ p) where
+  cast = P.subst₂ _⊆_ (reverse-involutive xs) (reverse-involutive ys)
+
+------------------------------------------------------------------------
+-- Inversion lemmas
+
+keep⁻¹ : ∀ {x y xs ys} → x ≈ y → (xs ⊆ ys) ⇔ (x ∷ xs ⊆ y ∷ ys)
+keep⁻¹ eq = equivalence (keep eq) (∷⁻ eq)
+
+skip⁻¹ : ∀ {x y xs ys} → ¬ (x ≈ y) → (x ∷ xs ⊆ ys) ⇔ (x ∷ xs ⊆ y ∷ ys)
+skip⁻¹ ¬eq = equivalence skip $ λ where
+  (skip p)     → p
+  (keep x≈y p) → ⊥-elim (¬eq x≈y)
+
+++⁻¹ : ∀ ps {xs ys} → (xs ⊆ ys) ⇔ (ps ++ xs ⊆ ps ++ ys)
+++⁻¹ ps = equivalence (++⁺ ⊆-refl) (++⁻ ps)
+
+------------------------------------------------------------------------
+-- Decidability of the order
+
+module Decidable (eq? : Decidable _≈_) where
+
+  infix 3 _⊆?_
+  _⊆?_ : Decidable _⊆_
+  []     ⊆? ys     = yes ([]⊆ ys)
+  x ∷ xs ⊆? []     = no λ ()
+  x ∷ xs ⊆? y ∷ ys with eq? x y
+  ... | yes x≈y = D.map (keep⁻¹ x≈y) (xs ⊆? ys)
+  ... | no ¬x≈y = D.map (skip⁻¹ ¬x≈y) (x ∷ xs ⊆? ys)
diff --git a/src/Data/List/Relation/Sublist/Inductive/Setoid/Solver.agda b/src/Data/List/Relation/Sublist/Inductive/Setoid/Solver.agda
new file mode 100644
index 0000000000..d6d59c5426
--- /dev/null
+++ b/src/Data/List/Relation/Sublist/Inductive/Setoid/Solver.agda
@@ -0,0 +1,149 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for proving that one list is a sublist of the other.
+------------------------------------------------------------------------
+
+open import Relation.Binary using (Decidable; Setoid)
+
+module Data.List.Relation.Sublist.Inductive.Setoid.Solver
+       {c ℓ} (S : Setoid c ℓ) where
+
+open import Data.Fin as Fin
+open import Data.Maybe as M
+open import Data.Nat as Nat
+open import Data.Product
+open import Data.Sum
+open import Data.Vec as Vec using (Vec ; lookup)
+open import Data.List hiding (lookup)
+open import Data.List.Properties
+open import Function
+open import Relation.Nullary
+import Relation.Binary.PropositionalEquality as PEq
+
+open import Data.Sum.Relation.Pointwise as Sum
+open import Data.List.Relation.Equality.Setoid S as ≋
+open import Data.List.Relation.Sublist.Inductive.Setoid S hiding (lookup)
+open import Data.List.Relation.Sublist.Inductive.Setoid.Properties S as ⊆
+
+open Setoid S renaming (Carrier to A)
+import Relation.Binary.EqReasoning as EqReasoning
+
+------------------------------------------------------------------------
+-- Reified list expressions
+
+-- Basic building blocks: variables and values
+-- We use Sum because it gets handy later on in the definition of `keep-it`:
+-- we can reuse the pointwise lifting of relations on Sums.
+Item : ℕ → Set c
+Item n = Fin n ⊎ A
+pattern var k = inj₁ k
+pattern val a = inj₂ a
+
+-- Abstract Syntax Trees
+infixr 5 _<>_
+data TList (n : ℕ) : Set c where
+  It   : Item n → TList n
+  _<>_ : TList n → TList n → TList n
+  []   : TList n
+
+-- Equivalent linearised representation
+RList : ℕ → Set c
+RList n = List (Item n)
+
+-- Semantics
+⟦_⟧I : ∀ {n} → Item n → Vec (List A) n → List A
+⟦ var k ⟧I ρ = lookup k ρ
+⟦ val a ⟧I ρ = [ a ]
+
+⟦_⟧T : ∀ {n} → TList n → Vec (List A) n → List A
+⟦ It it  ⟧T ρ = ⟦ it ⟧I ρ
+⟦ t <> u ⟧T ρ = ⟦ t ⟧T ρ ++ ⟦ u ⟧T ρ
+⟦ []     ⟧T ρ = []
+
+⟦_⟧R : ∀ {n} → RList n → Vec (List A) n → List A
+⟦ []     ⟧R ρ = []
+⟦ x ∷ xs ⟧R ρ = ⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ
+
+-- Orders
+_⊆T_ : ∀ {n} → (d e : TList n) → Set _
+d ⊆T e = ∀ ρ → ⟦ d ⟧T ρ ⊆ ⟦ e ⟧T ρ
+
+_⊆R_ : ∀ {n} → (d e : RList n) → Set _
+d ⊆R e = ∀ ρ → ⟦ d ⟧R ρ ⊆ ⟦ e ⟧R ρ
+
+-- Flattening in a semantics-respecting manner
+
+⟦++⟧R : ∀ {n} (xs ys : RList n) ρ → ⟦ xs ++ ys ⟧R ρ ≋ ⟦ xs ⟧R ρ ++ ⟦ ys ⟧R ρ
+⟦++⟧R []       ys ρ = ≋-refl
+⟦++⟧R (x ∷ xs) ys ρ = begin
+  ⟦ x ⟧I ρ ++ ⟦ xs ++ ys ⟧R ρ
+    ≈⟨ ≋.++⁺ ≋-refl (⟦++⟧R xs ys ρ) ⟩
+  ⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ ++ ⟦ ys ⟧R ρ
+    ≡⟨ PEq.sym $ ++-assoc (⟦ x ⟧I ρ) (⟦ xs ⟧R ρ) (⟦ ys ⟧R ρ) ⟩
+  (⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ) ++ ⟦ ys ⟧R ρ
+    ∎ where open EqReasoning ≋-setoid
+
+flatten : ∀ {n} (t : TList n) → Σ[ r ∈ RList n ] ∀ ρ → ⟦ t ⟧T ρ ≋ ⟦ r ⟧R ρ
+flatten []       = [] , λ _ → ≋-refl
+flatten (It it)  = it ∷ [] , λ ρ → ≋-reflexive (PEq.sym $ ++-identityʳ (⟦ It it ⟧T ρ))
+flatten (t <> u) =
+  let (rt , eqt) = flatten t
+      (ru , equ) = flatten u
+  in rt ++ ru , λ ρ → begin
+    ⟦ t <> u ⟧T ρ          ≡⟨⟩
+    ⟦ t ⟧T ρ ++ ⟦ u ⟧T ρ   ≈⟨ ≋.++⁺ (eqt ρ) (equ ρ) ⟩
+    ⟦ rt ⟧R ρ ++ ⟦ ru ⟧R ρ ≈⟨ ≋-sym $ ⟦++⟧R rt ru ρ ⟩
+    ⟦ rt ++ ru ⟧R ρ        ∎ where open EqReasoning ≋-setoid
+
+------------------------------------------------------------------------
+-- Solver for the sublist problem
+
+module _ {n : ℕ} (eq? : Decidable _≈_) where
+
+-- auxiliary lemmas
+
+  private
+
+    keep-it : ∀ {it it′} → Sum.Pointwise PEq._≡_ _≈_ it it′ →
+              (xs ys : RList n) → xs ⊆R ys → (it ∷ xs) ⊆R (it′ ∷ ys)
+    keep-it (₁∼₂ ())       xs ys hyp ρ
+    keep-it (₁∼₁ PEq.refl) xs ys hyp ρ = ⊆.++⁺ ⊆-refl (hyp ρ)
+    keep-it (₂∼₂ x≈y)      xs ys hyp ρ = ⊆.++⁺ (keep x≈y base) (hyp ρ)
+
+    skip-it : ∀ it (d e : RList n) → d ⊆R e → d ⊆R (it ∷ e)
+    skip-it it d ys hyp ρ = skips (⟦ it ⟧I ρ) (hyp ρ)
+
+-- Solver for linearised expressions
+
+  solveR : (d e : RList n) → Maybe (d ⊆R e)
+  -- trivial
+  solveR []          e           = just (λ ρ → []⊆ ⟦ e ⟧R ρ)
+  solveR (it ∷ d)    []          = nothing
+  -- actual work
+  solveR (var k ∷ d) (var l ∷ e) with k Fin.≟ l
+  ... | yes k≡l = M.map (keep-it (₁∼₁ k≡l) d e) (solveR d e)
+  ... | no ¬eq  = M.map (skip-it (var l) (var k ∷ d) e) (solveR (var k ∷ d) e)
+  solveR (val a ∷ d) (val b ∷ e) with eq? a b
+  ... | yes a≈b = M.map (keep-it (₂∼₂ a≈b) d e) (solveR d e)
+  ... | no ¬eq  = M.map (skip-it (val b) (val a ∷ d) e) (solveR (val a ∷ d) e)
+  solveR d (x ∷ e)               = M.map (skip-it x d e) (solveR d e)
+
+-- Coming back to ASTs thanks to flatten
+
+  solveT : (t u : TList n) → Maybe (t ⊆T u)
+  solveT t u =
+    let (rt , eqt) = flatten t
+        (ru , equ) = flatten u
+    in case solveR rt ru of λ where
+      nothing    → nothing
+      (just hyp) → just $′ λ ρ → begin
+        ⟦ t ⟧T ρ  ≋⟨ eqt ρ ⟩
+        ⟦ rt ⟧R ρ ⊆⟨ hyp ρ ⟩
+        ⟦ ru ⟧R ρ ≋⟨ ≋-sym (equ ρ) ⟩
+        ⟦ u ⟧T ρ  ∎ where open ⊆-Reasoning
+
+-- Prover for ASTs
+
+  prove : ∀ d e → From-just (solveT d e)
+  prove d e = from-just (solveT d e)
diff --git a/src/Data/List/Relation/Sublist/Inductive/Solver.agda b/src/Data/List/Relation/Sublist/Inductive/Solver.agda
deleted file mode 100644
index 80f1bec3a7..0000000000
--- a/src/Data/List/Relation/Sublist/Inductive/Solver.agda
+++ /dev/null
@@ -1,144 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- A solver for proving that one list is a sublist of the other.
-------------------------------------------------------------------------
-
-module Data.List.Relation.Sublist.Inductive.Solver where
-
-open import Data.Fin as Fin
-open import Data.Maybe as M
-open import Data.Nat as Nat
-open import Data.Product
-open import Data.Vec as Vec using (Vec ; lookup)
-open import Data.List hiding (lookup)
-open import Data.List.Properties
-open import Data.List.Relation.Sublist.Inductive hiding (lookup)
-open import Data.List.Relation.Sublist.Inductive.Properties
-open import Function
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality hiding ([_])
-open import Relation.Nullary
-
-open ≡-Reasoning
-
-------------------------------------------------------------------------
--- Reified list expressions
-
--- Basic building blocks: variables and values
-data Item {a} (n : ℕ) (A : Set a) : Set a where
-  var : Fin n → Item n A
-  val : A → Item n A
-
--- Abstract Syntax Trees
-infixr 5 _<>_
-data TList {a} (n : ℕ) (A : Set a) : Set a where
-  It   : Item n A → TList n A
-  _<>_ : TList n A → TList n A → TList n A
-  []   : TList n A
-
--- Equivalent linearised representation
-RList : ∀ {a} n → Set a → Set a
-RList n A = List (Item n A)
-
-module _ {n a} {A : Set a} where
-
--- Semantics
-  ⟦_⟧I : Item n A → Vec (List A) n → List A
-  ⟦ var k ⟧I ρ = lookup k ρ
-  ⟦ val a ⟧I ρ = [ a ]
-
-  ⟦_⟧T : TList n A → Vec (List A) n → List A
-  ⟦ It it  ⟧T ρ = ⟦ it ⟧I ρ
-  ⟦ t <> u ⟧T ρ = ⟦ t ⟧T ρ ++ ⟦ u ⟧T ρ
-  ⟦ []     ⟧T ρ = []
-
-  ⟦_⟧R : RList n A → Vec (List A) n → List A
-  ⟦ []     ⟧R ρ = []
-  ⟦ x ∷ xs ⟧R ρ = ⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ
-
--- Orders
-  _⊆T_ : (d e : TList n A) → Set a
-  d ⊆T e = ∀ ρ → ⟦ d ⟧T ρ ⊆ ⟦ e ⟧T ρ
-
-  _⊆R_ : (d e : RList n A) → Set a
-  d ⊆R e = ∀ ρ → ⟦ d ⟧R ρ ⊆ ⟦ e ⟧R ρ
-
--- Flattening in a semantics-respecting manner
-
-  ⟦++⟧R : ∀ xs ys ρ → ⟦ xs ++ ys ⟧R ρ ≡ ⟦ xs ⟧R ρ ++ ⟦ ys ⟧R ρ
-  ⟦++⟧R []       ys ρ = refl
-  ⟦++⟧R (x ∷ xs) ys ρ = begin
-    ⟦ x ⟧I ρ ++ ⟦ xs ++ ys ⟧R ρ
-      ≡⟨ cong (⟦ x ⟧I ρ ++_) (⟦++⟧R xs ys ρ) ⟩
-    ⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ ++ ⟦ ys ⟧R ρ
-      ≡⟨ sym $ ++-assoc (⟦ x ⟧I ρ) (⟦ xs ⟧R ρ) (⟦ ys ⟧R ρ) ⟩
-    (⟦ x ⟧I ρ ++ ⟦ xs ⟧R ρ) ++ ⟦ ys ⟧R ρ
-      ∎
-
-  flatten : ∀ (t : TList n A) → Σ[ r ∈ RList n A ] ⟦ t ⟧T ≗ ⟦ r ⟧R
-  flatten []       = [] , λ _ → refl
-  flatten (It it)  = it ∷ [] , λ ρ → sym $ ++-identityʳ (⟦ It it ⟧T ρ)
-  flatten (t <> u) =
-    let (rt , eqt) = flatten t
-        (ru , equ) = flatten u
-    in rt ++ ru , λ ρ → begin
-      ⟦ t <> u ⟧T ρ          ≡⟨⟩
-      ⟦ t ⟧T ρ ++ ⟦ u ⟧T ρ   ≡⟨ cong₂ _++_ (eqt ρ) (equ ρ) ⟩
-      ⟦ rt ⟧R ρ ++ ⟦ ru ⟧R ρ ≡⟨ sym $ ⟦++⟧R rt ru ρ ⟩
-      ⟦ rt ++ ru ⟧R ρ        ∎
-
-------------------------------------------------------------------------
--- Solver for the sublist problem
-
-module _ {n : ℕ} {a} {A : Set a} (eq? : Decidable {A = A} _≡_) where
-
--- auxiliary lemmas
-
-  private
-
-    keep-it : ∀ it (xs ys : RList n A) → xs ⊆R ys → (it ∷ xs) ⊆R (it ∷ ys)
-    keep-it it xs ys hyp ρ = ++⁺ ⊆-refl (hyp ρ)
-
-    skip-it : ∀ it (d e : RList n A) → d ⊆R e → d ⊆R (it ∷ e)
-    skip-it it d ys hyp ρ = skips (⟦ it ⟧I ρ) (hyp ρ)
-
--- Solver for linearised expressions
-
-  solveR : (d e : RList n A) → Maybe (d ⊆R e)
-  -- trivial
-  solveR []          e           = just (λ ρ → []⊆ ⟦ e ⟧R ρ)
-  solveR (it ∷ d)    []          = nothing
-  -- actual work
-  solveR (var k ∷ d) (var l ∷ e) with k Fin.≟ l
-  ... | yes refl = M.map (keep-it (var k) d e) (solveR d e)
-  ... | no ¬eq   = M.map (skip-it (var l) (var k ∷ d) e) (solveR (var k ∷ d) e)
-  solveR (val a ∷ d) (val b ∷ e) with eq? a b
-  ... | yes refl = M.map (keep-it (val a) d e) (solveR d e)
-  ... | no ¬eq   = M.map (skip-it (val b) (val a ∷ d) e) (solveR (val a ∷ d) e)
-  solveR d (x ∷ e)               = M.map (skip-it x d e) (solveR d e)
-
--- Coming back to ASTs thanks to flatten
-
-  solveT : (t u : TList n A) → Maybe (t ⊆T u)
-  solveT t u =
-    let (rt , eqt) = flatten t
-        (ru , equ) = flatten u
-    in case solveR rt ru of λ where
-      (just hyp) → just (λ ρ → subst₂ _⊆_ (sym (eqt ρ)) (sym (equ ρ)) (hyp ρ))
-      nothing    → nothing
-
--- Prover for ASTs
-
-  prove : ∀ d e → From-just (solveT d e)
-  prove d e = from-just (solveT d e)
-
-------------------------------------------------------------------------
--- Test
-
-_ : ∀ xs ys → xs ++ xs ⊆ (xs ++ 2 ∷ ys) ++ xs
-_ = λ xs ys →
-    let `xs = It (var zero)
-        `ys = It (var (suc zero))
-    in prove Nat._≟_ (`xs <> `xs) ((`xs <> It (val 2) <> `ys) <> `xs)
-                     (Vec.fromList (xs ∷ ys ∷ []))