diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3eebef2bca..ba99cf435c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,6 +30,28 @@ Deprecated names
   ∣-factors-≈  ↦  xy≈z⇒x|z∧y|z
   ```
 
+* In `Algebra.Solver.CommutativeMonoid`:
+  ```agda
+  normalise-correct  ↦  Algebra.Solver.CommutativeMonoid.Normal.correct
+  sg                 ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton
+  sg-correct         ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton-correct
+  ```
+
+* In `Algebra.Solver.IdempotentCommutativeMonoid`:
+  ```agda
+  flip12             ↦  Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz
+  distr              ↦  Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙
+  normalise-correct  ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct
+  sg                 ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton
+  sg-correct         ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton-correct
+  ```
+
+* In `Algebra.Solver.Monoid`:
+  ```agda
+  homomorphic        ↦  Algebra.Solver.Monoid.Normal.comp-correct
+  normalise-correct  ↦  Algebra.Solver.Monoid.Normal.correct
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   ++-assoc _      ↦  ++-assoc-eqFree
@@ -51,9 +73,28 @@ New modules
   Algebra.Properties.IdempotentCommutativeMonoid
   ```
 
+* Refactoring of the `Algebra.Solver.*Monoid` implementations, via
+  a single `Solver` module API based on the existing `Expr`, and
+  a common `Normal`-form API:
+  ```agda
+  Algebra.Solver.CommutativeMonoid.Normal
+  Algebra.Solver.IdempotentCommutativeMonoid.Normal
+  Algebra.Solver.Monoid.Expression
+  Algebra.Solver.Monoid.Normal
+  Algebra.Solver.Monoid.Solver
+  ```
+
+  NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.
+
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Solver.Ring`
+  ```agda
+  Env : ℕ → Set _
+  Env = Vec Carrier
+ ```
+
 * In `Data.List.Properties`:
   ```agda
   product≢0 : All NonZero ns → NonZero (product ns)
diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
index 04d4d372e6..9316418660 100644
--- a/src/Algebra/Solver/CommutativeMonoid.agda
+++ b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -8,196 +8,40 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (CommutativeMonoid)
 
-module Algebra.Solver.CommutativeMonoid {m₁ m₂} (M : CommutativeMonoid m₁ m₂) where
+module Algebra.Solver.CommutativeMonoid {c ℓ} (M : CommutativeMonoid c ℓ) where
 
-open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Maybe.Base as Maybe
-  using (Maybe; From-just; from-just)
-open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
-open import Data.Nat.GeneralisedArithmetic using (fold)
-open import Data.Product.Base using (_×_; uncurry)
-open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
+import Algebra.Solver.CommutativeMonoid.Normal as Normal
+import Algebra.Solver.Monoid.Solver as Solver
 
-open import Function.Base using (_∘_)
-
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-import Relation.Binary.Reflection as Reflection
-import Relation.Nullary.Decidable as Dec
-import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
-
-open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable as Dec using (Dec)
-
-open CommutativeMonoid M
-open ≈-Reasoning setoid
+open CommutativeMonoid M using (monoid)
 
 private
-  variable
-    n : ℕ
-
-------------------------------------------------------------------------
--- Monoid expressions
-
--- There is one constructor for every operation, plus one for
--- variables; there may be at most n variables.
-
-infixr 5 _⊕_
-infixr 10 _•_
-
-data Expr (n : ℕ) : Set where
-  var : Fin n → Expr n
-  id  : Expr n
-  _⊕_ : Expr n → Expr n → Expr n
-
--- An environment contains one value for every variable.
-
-Env : ℕ → Set _
-Env n = Vec Carrier n
-
--- The semantics of an expression is a function from an environment to
--- a value.
+  module N = Normal M
 
-⟦_⟧ : Expr n → Env n → Carrier
-⟦ var x   ⟧ ρ = lookup ρ x
-⟦ id      ⟧ ρ = ε
-⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
 
 ------------------------------------------------------------------------
 -- Normal forms
 
--- A normal form is a vector of multiplicities (a bag).
-
-Normal : ℕ → Set
-Normal n = Vec ℕ n
-
--- The semantics of a normal form.
-
-⟦_⟧⇓ : Normal n → Env n → Carrier
-⟦ []    ⟧⇓ _ = ε
-⟦ n ∷ v ⟧⇓ (a ∷ ρ) = fold (⟦ v ⟧⇓ ρ) (a ∙_) n
+open N public
+  renaming (correct to normalise-correct)
 
 ------------------------------------------------------------------------
--- Constructions on normal forms
-
--- The empty bag.
-
-empty : Normal n
-empty = replicate _ 0
-
--- A singleton bag.
+-- Proof procedures
 
-sg : (i : Fin n) → Normal n
-sg zero    = 1 ∷ empty
-sg (suc i) = 0 ∷ sg i
+open Solver monoid (record { N }) public
 
--- The composition of normal forms.
-
-_•_  : (v w : Normal n) → Normal n
-[]      • []      = []
-(l ∷ v) • (m ∷ w) = l + m ∷ v • w
 
 ------------------------------------------------------------------------
--- Correctness of the constructions on normal forms
-
--- The empty bag stands for the unit ε.
-
-empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
-empty-correct [] = refl
-empty-correct (a ∷ ρ) = empty-correct ρ
-
--- The singleton bag stands for a single variable.
-
-sg-correct : (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
-sg-correct zero (x ∷ ρ) = begin
-    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
-    x ∙ ε              ≈⟨ identityʳ _ ⟩
-    x                  ∎
-sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ
-
--- Normal form composition corresponds to the composition of the monoid.
-
-comp-correct : (v w : Normal n) (ρ : Env n) →
-              ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
-comp-correct [] [] ρ =  sym (identityˡ _)
-comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = lemma l m (comp-correct v w ρ)
-  where
-    flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c)
-    flip12 a b c = begin
-        a ∙ (b ∙ c)  ≈⟨ sym (assoc _ _ _) ⟩
-        (a ∙ b) ∙ c  ≈⟨ ∙-congʳ (comm _ _) ⟩
-        (b ∙ a) ∙ c  ≈⟨ assoc _ _ _ ⟩
-        b ∙ (a ∙ c)  ∎
-    lemma : ∀ l m {d b c} (p : d ≈ b ∙ c) →
-      fold d (a ∙_) (l + m) ≈ fold b (a ∙_) l ∙ fold c (a ∙_) m
-    lemma zero zero p = p
-    lemma zero (suc m) p = trans (∙-congˡ (lemma zero m p)) (flip12 _ _ _)
-    lemma (suc l) m p = trans (∙-congˡ (lemma l m p)) (sym (assoc a _ _))
-
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- Normalization
-
--- A normaliser.
-
-normalise : Expr n → Normal n
-normalise (var x)   = sg x
-normalise id        = empty
-normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂
-
--- The normaliser preserves the semantics of the expression.
-
-normalise-correct : (e : Expr n) (ρ : Env n) →
-    ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
-normalise-correct (var x)   ρ = sg-correct x ρ
-normalise-correct id        ρ = empty-correct ρ
-normalise-correct (e₁ ⊕ e₂) ρ =  begin
-
-    ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
-
-    ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩
-
-    ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
-  ∎
-
-------------------------------------------------------------------------
--- "Tactic.
-
-open module R = Reflection
-                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
-  public using (solve; _⊜_)
-
--- We can decide if two normal forms are /syntactically/ equal.
-
-infix 5 _≟_
-
-_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂)
-nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
-  where open Pointwise
-
--- We can also give a sound, but not necessarily complete, procedure
--- for determining if two expressions have the same semantics.
-
-prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
-prove′ e₁ e₂ =
-  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
-  where
-  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
-  lemma eq ρ =
-    R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
-      ⟦ normalise e₂ ⟧⇓ ρ  ∎)
-
--- This procedure can be combined with from-just.
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
-prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
-prove _ e₁ e₂ = from-just (prove′ e₁ e₂)
+-- Version 2.2
 
--- prove : ∀ n (es : Expr n × Expr n) →
---         From-just (uncurry prove′ es)
--- prove _ = from-just ∘ uncurry prove′
+{-# WARNING_ON_USAGE normalise-correct
+"Warning: normalise-correct was deprecated in v2.2.
+Please use Algebra.Solver.CommutativeMonoid.Normal.correct instead."
+#-}
diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda
new file mode 100644
index 0000000000..2d75ec21fe
--- /dev/null
+++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda
@@ -0,0 +1,161 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Normal forms in commutative monoids
+--
+-- Adapted from Algebra.Solver.Monoid.Normal
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (CommutativeMonoid)
+
+module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where
+
+import Algebra.Properties.CommutativeSemigroup as CSProperties
+import Algebra.Properties.Monoid.Mult as MultProperties
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat as ℕ using (ℕ; zero; suc; _+_)
+open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith)
+import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
+open import Relation.Binary.Definitions using (DecidableEquality)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Relation.Nullary.Decidable as Dec
+
+open CommutativeMonoid M
+open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+)
+open CSProperties commutativeSemigroup using (interchange)
+open ≈-Reasoning setoid
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+open import Algebra.Solver.Monoid.Expression rawMonoid public
+  hiding (NormalAPI)
+
+------------------------------------------------------------------------
+-- Normal forms
+
+-- A normal form is a vector of multiplicities (a bag).
+
+Normal : ℕ → Set
+Normal n = Vec ℕ n
+
+-- The semantics of a normal form.
+
+⟦_⟧⇓ : Normal n → Env n → Carrier
+⟦ []    ⟧⇓ _       = ε
+⟦ n ∷ v ⟧⇓ (a ∷ ρ) = (n × a) ∙ (⟦ v ⟧⇓ ρ)
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+infix 5 _≟_
+
+_≟_ : DecidableEquality (Normal n)
+nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂)
+  where open Pointwise using (Pointwise-≡↔≡; decidable)
+
+------------------------------------------------------------------------
+-- Constructions on normal forms
+
+-- The empty bag.
+
+empty : Normal n
+empty = replicate _ 0
+
+-- A singleton bag.
+
+singleton : (i : Fin n) → Normal n
+singleton zero    = 1 ∷ empty
+singleton (suc i) = 0 ∷ singleton i
+
+-- The composition of normal forms.
+infixr 10 _•_
+
+_•_  : (v w : Normal n) → Normal n
+_•_ = zipWith _+_
+
+------------------------------------------------------------------------
+-- Correctness of the constructions on normal forms
+
+-- The empty bag stands for the unit ε.
+
+empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
+empty-correct [] = refl
+empty-correct (a ∷ ρ) = begin
+    ε ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ identityˡ _ ⟩
+    ⟦ empty ⟧⇓ ρ       ≈⟨ empty-correct ρ ⟩
+    ε                  ∎
+
+-- The singleton bag stands for a single variable.
+
+singleton-correct : (x : Fin n) (ρ : Env n) →
+                    ⟦ singleton x ⟧⇓ ρ ≈ lookup ρ x
+singleton-correct zero (x ∷ ρ) = begin
+    (1 × x) ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congʳ (×-homo-1 _) ⟩
+    x ∙ ⟦ empty ⟧⇓ ρ         ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
+    x ∙ ε                    ≈⟨ identityʳ _ ⟩
+    x                        ∎
+singleton-correct (suc x) (m ∷ ρ) = begin
+    ε ∙ ⟦ singleton x ⟧⇓ ρ   ≈⟨ identityˡ _ ⟩
+    ⟦ singleton x ⟧⇓ ρ       ≈⟨ singleton-correct x ρ ⟩
+    lookup ρ x        ∎
+
+-- Normal form composition corresponds to the composition of the monoid.
+
+comp-correct : ∀ v w (ρ : Env n) →
+               ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
+comp-correct [] [] _ =  sym (identityˡ _)
+comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = begin
+  ((l + m) × a) ∙ ⟦ v • w ⟧⇓ ρ              ≈⟨ ∙-congʳ  (×-homo-+ a l m) ⟩
+  (l × a) ∙ (m × a) ∙ ⟦ v • w ⟧⇓ ρ          ≈⟨ ∙-congˡ  (comp-correct v w ρ) ⟩
+  (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ interchange _ _ _ _ ⟩
+  ⟦ l ∷ v ⟧⇓ (a ∷ ρ) ∙ ⟦ m ∷ w ⟧⇓ (a ∷ ρ)   ∎
+
+------------------------------------------------------------------------
+-- Normalization
+
+-- A normaliser.
+
+normalise : Expr n → Normal n
+normalise (var x)   = singleton x
+normalise id        = empty
+normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂
+
+-- The normaliser preserves the semantics of the expression.
+
+correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
+correct (var x)   ρ = singleton-correct x ρ
+correct id        ρ = empty-correct ρ
+correct (e₁ ⊕ e₂) ρ = begin
+  ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ
+    ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
+  ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
+    ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩
+  ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+    ∎
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.2
+
+sg = singleton
+{-# WARNING_ON_USAGE sg
+"Warning: sg was deprecated in v2.2.
+Please use singleton instead."
+#-}
+sg-correct = singleton-correct
+{-# WARNING_ON_USAGE sg-correct
+"Warning: sg-correct was deprecated in v2.2.
+Please use singleton-correct instead."
+#-}
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index 00b8824975..d5cac0585f 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -10,208 +10,39 @@
 
 open import Algebra.Bundles using (IdempotentCommutativeMonoid)
 
-open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
-open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.Maybe.Base as Maybe
-  using (Maybe; From-just; from-just)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_)
-open import Data.Product.Base using (_×_; uncurry)
-open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
-
-open import Function.Base using (_∘_)
-
-import Relation.Binary.Reasoning.Setoid  as ≈-Reasoning
-import Relation.Binary.Reflection            as Reflection
-import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
-
-open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
-open import Relation.Nullary.Decidable as Dec using (Dec)
-
-
 module Algebra.Solver.IdempotentCommutativeMonoid
-  {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where
-
-open IdempotentCommutativeMonoid M
-open ≈-Reasoning setoid
-
-private
-  variable
-    n : ℕ
-
-------------------------------------------------------------------------
--- Monoid expressions
-
--- There is one constructor for every operation, plus one for
--- variables; there may be at most n variables.
-
-infixr 5 _⊕_
-infixr 10 _•_
+  {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where
 
-data Expr (n : ℕ) : Set where
-  var : Fin n → Expr n
-  id  : Expr n
-  _⊕_ : Expr n → Expr n → Expr n
+import Algebra.Solver.IdempotentCommutativeMonoid.Normal as Normal
+import Algebra.Solver.Monoid.Solver as Solver
 
--- An environment contains one value for every variable.
+open IdempotentCommutativeMonoid M using (monoid)
 
-Env : ℕ → Set _
-Env n = Vec Carrier n
-
--- The semantics of an expression is a function from an environment to
--- a value.
+private
+  module N = Normal M
 
-⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier
-⟦ var x   ⟧ ρ = lookup ρ x
-⟦ id      ⟧ ρ = ε
-⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
 
 ------------------------------------------------------------------------
 -- Normal forms
 
--- A normal form is a vector of bits (a set).
-
-Normal : ℕ → Set
-Normal n = Vec Bool n
-
--- The semantics of a normal form.
-
-⟦_⟧⇓ : Normal n → Env n → Carrier
-⟦ []    ⟧⇓ _ = ε
-⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ)
-
-------------------------------------------------------------------------
--- Constructions on normal forms
-
--- The empty set.
-
-empty : Normal n
-empty = replicate _ false
-
--- A singleton set.
-
-sg : (i : Fin n) → Normal n
-sg zero    = true ∷ empty
-sg (suc i) = false ∷ sg i
-
--- The composition of normal forms.
-
-_•_ : (v w : Normal n) → Normal n
-[]      • []      = []
-(l ∷ v) • (m ∷ w) = (l ∨ m) ∷ v • w
+open N public
+  renaming (correct to normalise-correct)
 
 ------------------------------------------------------------------------
--- Correctness of the constructions on normal forms
-
--- The empty set stands for the unit ε.
-
-empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
-empty-correct []      = refl
-empty-correct (a ∷ ρ) = empty-correct ρ
-
--- The singleton set stands for a single variable.
-
-sg-correct : (x : Fin n) (ρ : Env n) → ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
-sg-correct zero (x ∷ ρ) = begin
-    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
-    x ∙ ε              ≈⟨ identityʳ _ ⟩
-    x                  ∎
-sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ
-
--- Normal form composition corresponds to the composition of the monoid.
+-- Proof procedures
 
-flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c)
-flip12 a b c = begin
-    a ∙ (b ∙ c)  ≈⟨ sym (assoc _ _ _) ⟩
-    (a ∙ b) ∙ c  ≈⟨ ∙-congʳ (comm _ _) ⟩
-    (b ∙ a) ∙ c  ≈⟨ assoc _ _ _ ⟩
-    b ∙ (a ∙ c)  ∎
+open Solver monoid (record { N }) public
 
-distr : ∀ a b c → a ∙ (b ∙ c) ≈ (a ∙ b) ∙ (a ∙ c)
-distr a b c = begin
-    a ∙ (b ∙ c)        ≈⟨ ∙-cong (sym (idem a)) refl ⟩
-    (a ∙ a) ∙ (b ∙ c)  ≈⟨ assoc _ _ _ ⟩
-    a ∙ (a ∙ (b ∙ c))  ≈⟨ ∙-congˡ (sym (assoc _ _ _)) ⟩
-    a ∙ ((a ∙ b) ∙ c)  ≈⟨ ∙-congˡ (∙-congʳ (comm _ _)) ⟩
-    a ∙ ((b ∙ a) ∙ c)  ≈⟨ ∙-congˡ (assoc _ _ _) ⟩
-    a ∙ (b ∙ (a ∙ c))  ≈⟨ sym (assoc _ _ _) ⟩
-    (a ∙ b) ∙ (a ∙ c)  ∎
-
-comp-correct : ∀ (v w : Normal n) (ρ : Env n) →
-              ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
-comp-correct [] [] ρ = sym (identityˡ _)
-comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) =
-  trans (∙-congˡ (comp-correct v w ρ)) (distr _ _ _)
-comp-correct (true ∷ v) (false ∷ w) (a ∷ ρ) =
-  trans (∙-congˡ (comp-correct v w ρ)) (sym (assoc _ _ _))
-comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) =
-  trans (∙-congˡ (comp-correct v w ρ)) (flip12 _ _ _)
-comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) =
-  comp-correct v w ρ
 
 ------------------------------------------------------------------------
--- Normalization
-
--- A normaliser.
-
-normalise : Expr n → Normal n
-normalise (var x)   = sg x
-normalise id        = empty
-normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂
-
--- The normaliser preserves the semantics of the expression.
-
-normalise-correct : (e : Expr n) (ρ : Env n) →
-    ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
-normalise-correct (var x)   ρ = sg-correct x ρ
-normalise-correct id        ρ = empty-correct ρ
-normalise-correct (e₁ ⊕ e₂) ρ = begin
-
-    ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
-
-    ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
-
-  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩
-
-    ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
-  ∎
-
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
--- "Tactic.
-
-open module R = Reflection
-                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
-  public using (solve; _⊜_)
-
--- We can decide if two normal forms are /syntactically/ equal.
-
-infix 5 _≟_
-
-_≟_ : (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂)
-nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂)
-  where open Pointwise
-
--- We can also give a sound, but not necessarily complete, procedure
--- for determining if two expressions have the same semantics.
-
-prove′ : (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
-prove′ e₁ e₂ =
-  Maybe.map lemma (dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂))
-  where
-  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
-  lemma eq ρ =
-    R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
-      ⟦ normalise e₂ ⟧⇓ ρ  ∎)
-
--- This procedure can be combined with from-just.
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
-prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
-prove _ e₁ e₂ = from-just (prove′ e₁ e₂)
+-- Version 2.2
 
--- prove : ∀ n (es : Expr n × Expr n) →
---         From-just (uncurry prove′ es)
--- prove _ = from-just ∘ uncurry prove′
+{-# WARNING_ON_USAGE normalise-correct
+"Warning: normalise-correct was deprecated in v2.2.
+Please use Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct instead."
+#-}
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda
new file mode 100644
index 0000000000..bb90c66c72
--- /dev/null
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda
@@ -0,0 +1,168 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Solver for equations in idempotent commutative monoids
+--
+-- Adapted from Algebra.Solver.CommutativeMonoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (IdempotentCommutativeMonoid)
+
+module Algebra.Solver.IdempotentCommutativeMonoid.Normal
+  {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where
+
+import Algebra.Properties.CommutativeSemigroup as CSProperties
+open import Algebra.Properties.IdempotentCommutativeMonoid M using (∙-distrˡ-∙)
+open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate; zipWith)
+import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
+open import Relation.Binary.Definitions using (DecidableEquality)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Relation.Nullary.Decidable       as Dec
+
+open IdempotentCommutativeMonoid M
+open CSProperties commutativeSemigroup using (x∙yz≈xy∙z; x∙yz≈y∙xz)
+open ≈-Reasoning setoid
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+open import Algebra.Solver.Monoid.Expression rawMonoid public
+  hiding (NormalAPI)
+
+------------------------------------------------------------------------
+-- Normal forms
+
+-- A normal form is a vector of bits (a set).
+
+Normal : ℕ → Set
+Normal n = Vec Bool n
+
+-- The semantics of a normal form.
+
+⟦_⟧⇓ : Normal n → Env n → Carrier
+⟦ []    ⟧⇓ _ = ε
+⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ)
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+infix 5 _≟_
+
+_≟_ : DecidableEquality (Normal n)
+nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂)
+  where open Pointwise using (Pointwise-≡↔≡; decidable)
+
+------------------------------------------------------------------------
+-- Constructions on normal forms
+
+-- The empty set.
+
+empty : Normal n
+empty = replicate _ false
+
+-- A singleton set.
+
+singleton : (i : Fin n) → Normal n
+singleton zero    = true ∷ empty
+singleton (suc i) = false ∷ singleton i
+
+-- The composition of normal forms.
+infixr 10 _•_
+
+_•_ : (v w : Normal n) → Normal n
+_•_ = zipWith _∨_
+
+------------------------------------------------------------------------
+-- Correctness of the constructions on normal forms
+
+-- The empty set stands for the unit ε.
+
+empty-correct : (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
+empty-correct []      = refl
+empty-correct (a ∷ ρ) = empty-correct ρ
+
+-- The singleton set stands for a single variable.
+
+singleton-correct : (x : Fin n) (ρ : Env n) →
+                    ⟦ singleton x ⟧⇓ ρ ≈ lookup ρ x
+singleton-correct zero (x ∷ ρ) = begin
+    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
+    x ∙ ε              ≈⟨ identityʳ _ ⟩
+    x                  ∎
+singleton-correct (suc x) (m ∷ ρ) = singleton-correct x ρ
+
+-- Normal form composition corresponds to the composition of the monoid.
+
+comp-correct : ∀ v w (ρ : Env n) →
+               ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
+comp-correct [] [] ρ = sym (identityˡ _)
+comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) =
+  trans (∙-congˡ (comp-correct v w ρ)) (∙-distrˡ-∙ _ _ _)
+comp-correct (true ∷ v) (false ∷ w) (a ∷ ρ) =
+  trans (∙-congˡ (comp-correct v w ρ)) (x∙yz≈xy∙z _ _ _)
+comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) =
+  trans (∙-congˡ (comp-correct v w ρ)) (x∙yz≈y∙xz _ _ _)
+comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) =
+  comp-correct v w ρ
+
+------------------------------------------------------------------------
+-- Normalization
+
+-- A normaliser.
+
+normalise : Expr n → Normal n
+normalise (var x)   = singleton x
+normalise id        = empty
+normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂
+
+-- The normaliser preserves the semantics of the expression.
+
+correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
+correct (var x)   ρ = singleton-correct x ρ
+correct id        ρ = empty-correct ρ
+correct (e₁ ⊕ e₂) ρ = begin
+  ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ
+    ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
+  ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ
+    ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩
+  ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+    ∎
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.2
+
+flip12 = x∙yz≈y∙xz
+{-# WARNING_ON_USAGE flip12
+"Warning: flip12 was deprecated in v2.2.
+Please use Algebra.Properties.CommutativeSemigroup.x∙yz≈y∙xz instead."
+#-}
+distr = ∙-distrˡ-∙
+{-# WARNING_ON_USAGE distr
+"Warning: distr was deprecated in v2.2.
+Please use Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙ instead."
+#-}
+sg = singleton
+{-# WARNING_ON_USAGE sg
+"Warning: sg was deprecated in v2.2.
+Please use singleton instead."
+#-}
+sg-correct = singleton-correct
+{-# WARNING_ON_USAGE sg-correct
+"Warning: sg-correct was deprecated in v2.2.
+Please use singleton-correct instead."
+#-}
diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
index 7debc4e1aa..f0ee5ca799 100644
--- a/src/Algebra/Solver/Monoid.agda
+++ b/src/Algebra/Solver/Monoid.agda
@@ -6,133 +6,51 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (Monoid)
 
-module Algebra.Solver.Monoid {m₁ m₂} (M : Monoid m₁ m₂) where
+module Algebra.Solver.Monoid {c ℓ} (M : Monoid c ℓ) where
 
-open import Data.Fin.Base as Fin
-import Data.Fin.Properties as Fin
-open import Data.List.Base hiding (lookup)
-import Data.List.Relation.Binary.Equality.DecPropositional as ListEq
+import Algebra.Solver.Monoid.Normal as Normal
+import Algebra.Solver.Monoid.Solver as Solver
 open import Data.Maybe.Base as Maybe
-  using (Maybe; From-just; from-just)
-open import Data.Nat.Base using (ℕ)
+  using (From-just; from-just)
 open import Data.Product.Base using (_×_; uncurry)
-open import Data.Vec.Base using (Vec; lookup)
-open import Function.Base using (_∘_; _$_)
-open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-open import Relation.Binary.Definitions using (DecidableEquality)
+open import Function.Base using (_∘_)
 
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
-import Relation.Binary.Reflection
-import Relation.Nullary.Decidable.Core as Dec
+private
+  module N = Normal M
 
-open Monoid M
-open import Relation.Binary.Reasoning.Setoid setoid
-
-------------------------------------------------------------------------
--- Monoid expressions
-
--- There is one constructor for every operation, plus one for
--- variables; there may be at most n variables.
-
-infixr 5 _⊕_
-
-data Expr (n : ℕ) : Set where
-  var : Fin n → Expr n
-  id  : Expr n
-  _⊕_ : Expr n → Expr n → Expr n
-
--- An environment contains one value for every variable.
-
-Env : ℕ → Set _
-Env n = Vec Carrier n
-
--- The semantics of an expression is a function from an environment to
--- a value.
-
-⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier
-⟦ var x   ⟧ ρ = lookup ρ x
-⟦ id      ⟧ ρ = ε
-⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
 
 ------------------------------------------------------------------------
 -- Normal forms
 
--- A normal form is a list of variables.
-
-Normal : ℕ → Set
-Normal n = List (Fin n)
-
--- The semantics of a normal form.
-
-⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier
-⟦ []     ⟧⇓ ρ = ε
-⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ
-
--- A normaliser.
-
-normalise : ∀ {n} → Expr n → Normal n
-normalise (var x)   = x ∷ []
-normalise id        = []
-normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂
-
--- The normaliser is homomorphic with respect to _++_/_∙_.
-
-homomorphic : ∀ {n} (nf₁ nf₂ : Normal n) (ρ : Env n) →
-              ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)
-homomorphic [] nf₂ ρ = begin
-  ⟦ nf₂ ⟧⇓ ρ      ≈⟨ sym $ identityˡ _ ⟩
-  ε ∙ ⟦ nf₂ ⟧⇓ ρ  ∎
-homomorphic (x ∷ nf₁) nf₂ ρ = begin
-  lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ          ≈⟨ ∙-congˡ (homomorphic nf₁ nf₂ ρ) ⟩
-  lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)  ≈⟨ sym $ assoc _ _ _ ⟩
-  lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ    ∎
-
--- The normaliser preserves the semantics of the expression.
-
-normalise-correct :
-  ∀ {n} (e : Expr n) (ρ : Env n) → ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
-normalise-correct (var x) ρ = begin
-  lookup ρ x ∙ ε  ≈⟨ identityʳ _ ⟩
-  lookup ρ x      ∎
-normalise-correct id ρ = begin
-  ε  ∎
-normalise-correct (e₁ ⊕ e₂) ρ = begin
-  ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ        ≈⟨ homomorphic (normalise e₁) (normalise e₂) ρ ⟩
-  ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩
-  ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ                        ∎
+open N public
+  renaming (comp-correct to homomorphic; correct to normalise-correct)
 
 ------------------------------------------------------------------------
--- "Tactic.
+-- Tactic
 
-open module R = Relation.Binary.Reflection
-                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
-  public using (solve; _⊜_)
+open Solver M (record { N }) public
+  hiding (prove)
 
--- We can decide if two normal forms are /syntactically/ equal.
-
-infix 5 _≟_
+prove : ∀ n (es : Expr n × Expr n) → From-just (uncurry prove′ es)
+prove _ = from-just ∘ uncurry prove′
 
-_≟_ : ∀ {n} → DecidableEquality (Normal n)
-nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
-  where open ListEq Fin._≟_
 
--- We can also give a sound, but not necessarily complete, procedure
--- for determining if two expressions have the same semantics.
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
-prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
-prove′ e₁ e₂ =
-  Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)
-  where
-  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
-  lemma eq ρ =
-    R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
-      ⟦ normalise e₂ ⟧⇓ ρ  ∎)
+-- Version 2.2
 
--- This procedure can be combined with from-just.
+{-# WARNING_ON_USAGE homomorphic
+"Warning: homomorphic was deprecated in v2.2.
+Please use Algebra.Solver.Monoid.Normal.comp-correct instead."
+#-}
 
-prove : ∀ n (es : Expr n × Expr n) →
-        From-just (uncurry prove′ es)
-prove _ = from-just ∘ uncurry prove′
+{-# WARNING_ON_USAGE normalise-correct
+"Warning: normalise-correct was deprecated in v2.2.
+Please use Algebra.Solver.Monoid.Normal.correct instead."
+#-}
diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda
new file mode 100644
index 0000000000..7b71c9e9c2
--- /dev/null
+++ b/src/Algebra/Solver/Monoid/Expression.agda
@@ -0,0 +1,69 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for equations over monoids
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles.Raw using (RawMonoid)
+
+module Algebra.Solver.Monoid.Expression {c ℓ} (M : RawMonoid c ℓ) where
+
+open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Base using (Vec; lookup)
+open import Level using (suc; _⊔_)
+open import Relation.Binary.Definitions using (DecidableEquality)
+
+open RawMonoid M
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+-- There is one constructor for every operation, plus one for
+-- variables; there may be at most n variables.
+
+infixr 5 _⊕_
+
+data Expr (n : ℕ) : Set where
+  var : Fin n → Expr n
+  id  : Expr n
+  _⊕_ : Expr n → Expr n → Expr n
+
+-- An environment contains one value for every variable.
+
+Env : ℕ → Set _
+Env n = Vec Carrier n
+
+-- The semantics of an expression is a function from an environment to
+-- a value.
+
+⟦_⟧ : Expr n → Env n → Carrier
+⟦ var x   ⟧ ρ = lookup ρ x
+⟦ id      ⟧ ρ = ε
+⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
+
+------------------------------------------------------------------------
+-- API for normal expressions
+
+record NormalAPI a : Set (suc a ⊔ c ⊔ ℓ) where
+  infix 5 _≟_
+
+  field
+
+-- The type of normal forms.
+    Normal    : ℕ → Set a
+-- We can decide if two normal forms are /syntactically/ equal.
+    _≟_       : DecidableEquality (Normal n)
+-- A normaliser.
+    normalise : Expr n → Normal n
+-- The semantics of a normal form.
+    ⟦_⟧⇓      : Normal n → Env n → Carrier
+-- The normaliser preserves the semantics of the expression.
+    correct   : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
+
diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda
new file mode 100644
index 0000000000..6fd4f3e839
--- /dev/null
+++ b/src/Algebra/Solver/Monoid/Normal.agda
@@ -0,0 +1,89 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for equations over monoids
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Monoid)
+
+module Algebra.Solver.Monoid.Normal {c ℓ} (M : Monoid c ℓ) where
+
+open import Data.Fin.Base using (Fin)
+import Data.Fin.Properties as Fin
+open import Data.List.Base using (List; [] ; _∷_; _++_)
+import Data.List.Relation.Binary.Equality.DecPropositional as ≋
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Base using (lookup)
+open import Function.Base using (_∘_; _$_)
+open import Relation.Binary.Definitions using (DecidableEquality)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Relation.Nullary.Decidable as Dec
+
+open Monoid M
+open ≈-Reasoning setoid
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Monoid expressions
+
+open import Algebra.Solver.Monoid.Expression rawMonoid public
+
+------------------------------------------------------------------------
+-- Normal forms
+
+-- A normal form is a list of variables.
+
+Normal : ℕ → Set _
+Normal n = List (Fin n)
+
+-- The semantics of a normal form.
+
+⟦_⟧⇓ : Normal n → Env n → Carrier
+⟦ []     ⟧⇓ ρ = ε
+⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ
+
+-- We can decide if two normal forms are /syntactically/ equal.
+
+infix 5 _≟_
+
+_≟_ : DecidableEquality (Normal n)
+nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
+  where open ≋ Fin._≟_ using (_≋?_; ≋⇒≡; ≡⇒≋)
+
+-- A normaliser.
+
+normalise : Expr n → Normal n
+normalise (var x)   = x ∷ []
+normalise id        = []
+normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂
+
+-- The normaliser is homomorphic with respect to _++_/_∙_.
+
+comp-correct : ∀ nf₁ nf₂ (ρ : Env n) →
+              ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)
+comp-correct [] nf₂ ρ = begin
+  ⟦ nf₂ ⟧⇓ ρ      ≈⟨ identityˡ _ ⟨
+  ε ∙ ⟦ nf₂ ⟧⇓ ρ  ∎
+comp-correct (x ∷ nf₁) nf₂ ρ = begin
+  lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ          ≈⟨ ∙-congˡ (comp-correct nf₁ nf₂ ρ) ⟩
+  lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)  ≈⟨ assoc _ _ _ ⟨
+  lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ    ∎
+
+-- The normaliser preserves the semantics of the expression.
+
+correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
+correct (var x) ρ = begin
+  lookup ρ x ∙ ε  ≈⟨ identityʳ _ ⟩
+  lookup ρ x      ∎
+correct id ρ = begin
+  ε  ∎
+correct (e₁ ⊕ e₂) ρ = begin
+  ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ        ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
+  ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ  ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩
+  ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ                        ∎
diff --git a/src/Algebra/Solver/Monoid/Solver.agda b/src/Algebra/Solver/Monoid/Solver.agda
new file mode 100644
index 0000000000..a1281e9639
--- /dev/null
+++ b/src/Algebra/Solver/Monoid/Solver.agda
@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for equations over monoids
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (Monoid)
+import Algebra.Solver.Monoid.Expression as Expression
+
+module Algebra.Solver.Monoid.Solver {a c ℓ} (M : Monoid c ℓ)
+  (open Monoid M using (rawMonoid; setoid; _≈_))
+  (open Expression rawMonoid using (Expr; Env; var; ⟦_⟧; NormalAPI))
+  (N : NormalAPI a) where
+
+open import Data.Maybe.Base as Maybe
+  using (Maybe; From-just; from-just)
+open import Data.Nat.Base using (ℕ)
+open import Function.Base using (_∘_; _$_)
+open import Relation.Binary.Consequences using (dec⇒weaklyDec)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
+import Relation.Binary.Reflection as Reflection
+
+open NormalAPI N
+
+private
+  variable
+    n : ℕ
+  module
+    R = Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct
+
+
+------------------------------------------------------------------------
+-- Proof procedures
+
+-- Re-export the existing solver machinery from `Reflection`
+
+open R public
+  using (solve; _⊜_)
+
+-- We can also give a sound, but not necessarily complete, procedure
+-- for determining if two expressions have the same semantics.
+
+prove′ : ∀ e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
+prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)
+  where
+  open import Relation.Binary.Reasoning.Setoid setoid
+  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
+  lemma eq ρ = R.prove ρ e₁ e₂ $ begin
+    ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
+    ⟦ normalise e₂ ⟧⇓ ρ  ∎
+
+-- This procedure can then be combined with from-just.
+
+prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
+prove _ e₁ e₂ = from-just $ prove′ e₁ e₂
diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda
index a2a982d5c2..4d31bf5442 100644
--- a/src/Algebra/Solver/Ring.agda
+++ b/src/Algebra/Solver/Ring.agda
@@ -58,6 +58,11 @@ infixl 8 _:*_ _*N_ _*H_ _*NH_ _*HN_
 infixl 7 _:+_ _:-_ _+H_ _+N_
 infix  4 _≈H_ _≈N_
 
+private
+  variable
+    n : ℕ
+
+
 ------------------------------------------------------------------------
 -- Polynomials
 
@@ -76,16 +81,16 @@ data Polynomial (m : ℕ) : Set r₁ where
 
 -- Short-hand notation.
 
-_:+_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
+_:+_ : Polynomial n → Polynomial n → Polynomial n
 _:+_ = op [+]
 
-_:*_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
+_:*_ : Polynomial n → Polynomial n → Polynomial n
 _:*_ = op [*]
 
-_:-_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
+_:-_ : Polynomial n → Polynomial n → Polynomial n
 x :- y = x :+ :- y
 
-_:×_ : ∀ {n} → ℕ → Polynomial n → Polynomial n
+_:×_ : ℕ → Polynomial n → Polynomial n
 zero :× p = con C.0#
 suc m :× p = p :+ m :× p
 
@@ -95,7 +100,12 @@ sem : Op → Op₂ Carrier
 sem [+] = _+_
 sem [*] = _*_
 
-⟦_⟧ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier
+-- An environment contains one value for every variable.
+
+Env : ℕ → Set _
+Env = Vec Carrier
+
+⟦_⟧ : Polynomial n → Env n → Carrier
 ⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ
 ⟦ con c      ⟧ ρ = ⟦ c ⟧′
 ⟦ var x      ⟧ ρ = lookup ρ x
@@ -132,12 +142,12 @@ mutual
   -- degree.
 
   data HNF : ℕ → Set r₁ where
-    ∅     : ∀ {n} → HNF (suc n)
-    _*x+_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
+    ∅     : HNF (suc n)
+    _*x+_ : HNF (suc n) → Normal n → HNF (suc n)
 
   data Normal : ℕ → Set r₁ where
     con  : C.Carrier → Normal zero
-    poly : ∀ {n} → HNF (suc n) → Normal (suc n)
+    poly : HNF (suc n) → Normal (suc n)
 
   -- Note that the data types above do /not/ ensure uniqueness of
   -- normal forms: the zero polynomial of degree one can be
@@ -147,11 +157,11 @@ mutual
 
   -- Semantics.
 
-  ⟦_⟧H : ∀ {n} → HNF (suc n) → Vec Carrier (suc n) → Carrier
+  ⟦_⟧H : HNF (suc n) → Env (suc n) → Carrier
   ⟦ ∅       ⟧H _       = 0#
   ⟦ p *x+ c ⟧H (x ∷ ρ) = ⟦ p ⟧H (x ∷ ρ) * x + ⟦ c ⟧N ρ
 
-  ⟦_⟧N : ∀ {n} → Normal n → Vec Carrier n → Carrier
+  ⟦_⟧N : Normal n → Env n → Carrier
   ⟦ con c  ⟧N _ = ⟦ c ⟧′
   ⟦ poly p ⟧N ρ = ⟦ p ⟧H ρ
 
@@ -162,12 +172,12 @@ mutual
 
   -- Equality.
 
-  data _≈H_ : ∀ {n} → HNF n → HNF n → Set (r₁ ⊔ r₃) where
-    ∅     : ∀ {n} → _≈H_ {suc n} ∅ ∅
+  data _≈H_ : HNF n → HNF n → Set (r₁ ⊔ r₃) where
+    ∅     : _≈H_ {suc n} ∅ ∅
     _*x+_ : ∀ {n} {p₁ p₂ : HNF (suc n)} {c₁ c₂ : Normal n} →
             p₁ ≈H p₂ → c₁ ≈N c₂ → (p₁ *x+ c₁) ≈H (p₂ *x+ c₂)
 
-  data _≈N_ : ∀ {n} → Normal n → Normal n → Set (r₁ ⊔ r₃) where
+  data _≈N_ : Normal n → Normal n → Set (r₁ ⊔ r₃) where
     con  : ∀ {c₁ c₂} → ⟦ c₁ ⟧′ ≈ ⟦ c₂ ⟧′ → con c₁ ≈N con c₂
     poly : ∀ {n} {p₁ p₂ : HNF (suc n)} → p₁ ≈H p₂ → poly p₁ ≈N poly p₂
 
@@ -177,7 +187,7 @@ mutual
 
   infix 4 _≟H_ _≟N_
 
-  _≟H_ : ∀ {n} → WeaklyDecidable (_≈H_ {n = n})
+  _≟H_ : WeaklyDecidable (_≈H_ {n = n})
   ∅           ≟H ∅           = just ∅
   ∅           ≟H (_ *x+ _)   = nothing
   (_ *x+ _)   ≟H ∅           = nothing
@@ -186,7 +196,7 @@ mutual
   ... | _          | nothing    = nothing
   ... | nothing    | _          = nothing
 
-  _≟N_ : ∀ {n} → WeaklyDecidable (_≈N_ {n = n})
+  _≟N_ : WeaklyDecidable (_≈N_ {n = n})
   con c₁ ≟N con c₂ with c₁ coeff≟ c₂
   ... | just c₁≈c₂ = just (con c₁≈c₂)
   ... | nothing    = nothing
@@ -198,7 +208,7 @@ mutual
 
   -- The semantics respect the equality relations defined above.
 
-  ⟦_⟧H-cong : ∀ {n} {p₁ p₂ : HNF (suc n)} →
+  ⟦_⟧H-cong : {p₁ p₂ : HNF (suc n)} →
               p₁ ≈H p₂ → ∀ ρ → ⟦ p₁ ⟧H ρ ≈ ⟦ p₂ ⟧H ρ
   ⟦ ∅               ⟧H-cong _       = refl
   ⟦ p₁≈p₂ *x+ c₁≈c₂ ⟧H-cong (x ∷ ρ) =
@@ -206,9 +216,8 @@ mutual
       ⟨ +-cong ⟩
     ⟦ c₁≈c₂ ⟧N-cong ρ
 
-  ⟦_⟧N-cong :
-    ∀ {n} {p₁ p₂ : Normal n} →
-    p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ
+  ⟦_⟧N-cong : {p₁ p₂ : Normal n} →
+              p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ
   ⟦ con c₁≈c₂  ⟧N-cong _ = c₁≈c₂
   ⟦ poly p₁≈p₂ ⟧N-cong ρ = ⟦ p₁≈p₂ ⟧H-cong ρ
 
@@ -217,10 +226,10 @@ mutual
 
 -- Zero.
 
-0H : ∀ {n} → HNF (suc n)
+0H : HNF (suc n)
 0H = ∅
 
-0N : ∀ {n} → Normal n
+0N : Normal n
 0N {zero}  = con C.0#
 0N {suc n} = poly 0H
 
@@ -228,16 +237,16 @@ mutual
 
   -- One.
 
-  1H : ∀ {n} → HNF (suc n)
+  1H : HNF (suc n)
   1H {n} = ∅ *x+ 1N {n}
 
-  1N : ∀ {n} → Normal n
+  1N : Normal n
   1N {zero}  = con C.1#
   1N {suc n} = poly 1H
 
 -- A simplifying variant of _*x+_.
 
-_*x+HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
+_*x+HN_ : HNF (suc n) → Normal n → HNF (suc n)
 (p *x+ c′) *x+HN c = (p *x+ c′) *x+ c
 ∅          *x+HN c with c ≟N 0N
 ... | just c≈0 = ∅
@@ -247,49 +256,49 @@ mutual
 
   -- Addition.
 
-  _+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
+  _+H_ : HNF (suc n) → HNF (suc n) → HNF (suc n)
   ∅           +H p           = p
   p           +H ∅           = p
   (p₁ *x+ c₁) +H (p₂ *x+ c₂) = (p₁ +H p₂) *x+HN (c₁ +N c₂)
 
-  _+N_ : ∀ {n} → Normal n → Normal n → Normal n
+  _+N_ : Normal n → Normal n → Normal n
   con c₁  +N con c₂  = con (c₁ C.+ c₂)
   poly p₁ +N poly p₂ = poly (p₁ +H p₂)
 
 -- Multiplication.
 
-_*x+H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
+_*x+H_ : HNF (suc n) → HNF (suc n) → HNF (suc n)
 p₁         *x+H (p₂ *x+ c) = (p₁ +H p₂) *x+HN c
 ∅          *x+H ∅          = ∅
 (p₁ *x+ c) *x+H ∅          = (p₁ *x+ c) *x+ 0N
 
 mutual
 
-  _*NH_ : ∀ {n} → Normal n → HNF (suc n) → HNF (suc n)
+  _*NH_ : Normal n → HNF (suc n) → HNF (suc n)
   c *NH ∅          = ∅
   c *NH (p *x+ c′) with c ≟N 0N
   ... | just c≈0 = ∅
   ... | nothing  = (c *NH p) *x+ (c *N c′)
 
-  _*HN_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)
+  _*HN_ : HNF (suc n) → Normal n → HNF (suc n)
   ∅          *HN c = ∅
   (p *x+ c′) *HN c with c ≟N 0N
   ... | just c≈0 = ∅
   ... | nothing  = (p *HN c) *x+ (c′ *N c)
 
-  _*H_ : ∀ {n} → HNF (suc n) → HNF (suc n) → HNF (suc n)
+  _*H_ : HNF (suc n) → HNF (suc n) → HNF (suc n)
   ∅           *H _           = ∅
   (_ *x+ _)   *H ∅           = ∅
   (p₁ *x+ c₁) *H (p₂ *x+ c₂) =
     ((p₁ *H p₂) *x+H (p₁ *HN c₂ +H c₁ *NH p₂)) *x+HN (c₁ *N c₂)
 
-  _*N_ : ∀ {n} → Normal n → Normal n → Normal n
+  _*N_ : Normal n → Normal n → Normal n
   con c₁  *N con c₂  = con (c₁ C.* c₂)
   poly p₁ *N poly p₂ = poly (p₁ *H p₂)
 
 -- Exponentiation.
 
-_^N_ : ∀ {n} → Normal n → ℕ → Normal n
+_^N_ : Normal n → ℕ → Normal n
 p ^N zero  = 1N
 p ^N suc n = p *N (p ^N n)
 
@@ -297,25 +306,25 @@ mutual
 
   -- Negation.
 
-  -H_ : ∀ {n} → HNF (suc n) → HNF (suc n)
+  -H_ : HNF (suc n) → HNF (suc n)
   -H p = (-N 1N) *NH p
 
-  -N_ : ∀ {n} → Normal n → Normal n
+  -N_ : Normal n → Normal n
   -N con c  = con (C.- c)
   -N poly p = poly (-H p)
 
 ------------------------------------------------------------------------
 -- Normalisation
 
-normalise-con : ∀ {n} → C.Carrier → Normal n
+normalise-con : C.Carrier → Normal n
 normalise-con {zero}  c = con c
 normalise-con {suc n} c = poly (∅ *x+HN normalise-con c)
 
-normalise-var : ∀ {n} → Fin n → Normal n
+normalise-var : Fin n → Normal n
 normalise-var zero    = poly ((∅ *x+ 1N) *x+ 0N)
 normalise-var (suc i) = poly (∅ *x+HN normalise-var i)
 
-normalise : ∀ {n} → Polynomial n → Normal n
+normalise : Polynomial n → Normal n
 normalise (op [+] t₁ t₂) = normalise t₁ +N normalise t₂
 normalise (op [*] t₁ t₂) = normalise t₁ *N normalise t₂
 normalise (con c)        = normalise-con c
@@ -325,7 +334,7 @@ normalise (:- t)         = -N normalise t
 
 -- Evaluation after normalisation.
 
-⟦_⟧↓ : ∀ {n} → Polynomial n → Vec Carrier n → Carrier
+⟦_⟧↓ : Polynomial n → Env n → Carrier
 ⟦ p ⟧↓ ρ = ⟦ normalise p ⟧N ρ
 
 ------------------------------------------------------------------------
@@ -502,7 +511,7 @@ mutual
 ------------------------------------------------------------------------
 -- Correctness
 
-correct-con : ∀ {n} (c : C.Carrier) (ρ : Vec Carrier n) →
+correct-con : ∀ {n} (c : C.Carrier) (ρ : Env n) →
               ⟦ normalise-con c ⟧N ρ ≈ ⟦ c ⟧′
 correct-con c []      = refl
 correct-con c (x ∷ ρ) = begin
diff --git a/src/Relation/Binary/Reflection.agda b/src/Relation/Binary/Reflection.agda
index 12665df8cc..cf7cf77e11 100644
--- a/src/Relation/Binary/Reflection.agda
+++ b/src/Relation/Binary/Reflection.agda
@@ -10,11 +10,10 @@
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base using (ℕ)
 open import Data.Vec.Base as Vec using (Vec; allFin)
-open import Function.Base using (id; _⟨_⟩_)
+open import Function.Base using (id)
 open import Function.Bundles using (module Equivalence)
 open import Level using (Level)
 open import Relation.Binary.Bundles using (Setoid)
-import Relation.Binary.PropositionalEquality.Core as ≡
 
 -- Think of the parameters as follows:
 --
@@ -33,18 +32,17 @@ import Relation.Binary.PropositionalEquality.Core as ≡
 module Relation.Binary.Reflection
          {e a s}
          {Expr : ℕ → Set e} {A : Set a}
-         (Sem : Setoid a s)
+         (Sem : Setoid a s) (open Setoid Sem using (Carrier; _≈_))
          (var : ∀ {n} → Fin n → Expr n)
-         (⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Setoid.Carrier Sem)
-         (correct : ∀ {n} (e : Expr n) ρ →
-                    ⟦ e ⇓⟧ ρ ⟨ Setoid._≈_ Sem ⟩ ⟦ e ⟧ ρ)
+         (⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Carrier)
+         (correct : ∀ {n} (e : Expr n) ρ → ⟦ e ⇓⟧ ρ ≈ ⟦ e ⟧ ρ)
          where
 
 open import Data.Vec.N-ary
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+import Relation.Binary.PropositionalEquality.Core as ≡
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-open Setoid Sem
 open ≈-Reasoning Sem
 
 -- If two normalised expressions are semantically equal, then their
@@ -54,7 +52,7 @@ prove : ∀ {n} (ρ : Vec A n) e₁ e₂ →
         ⟦ e₁ ⇓⟧ ρ ≈ ⟦ e₂ ⇓⟧ ρ →
         ⟦ e₁  ⟧ ρ ≈ ⟦ e₂  ⟧ ρ
 prove ρ e₁ e₂ hyp = begin
-  ⟦ e₁  ⟧ ρ ≈⟨ sym (correct e₁ ρ) ⟩
+  ⟦ e₁  ⟧ ρ ≈⟨ correct e₁ ρ ⟨
   ⟦ e₁ ⇓⟧ ρ ≈⟨ hyp ⟩
   ⟦ e₂ ⇓⟧ ρ ≈⟨ correct e₂ ρ ⟩
   ⟦ e₂  ⟧ ρ ∎
diff --git a/src/Tactic/RingSolver.agda b/src/Tactic/RingSolver.agda
index 59475a3129..9c6cb29e8e 100644
--- a/src/Tactic/RingSolver.agda
+++ b/src/Tactic/RingSolver.agda
@@ -20,7 +20,6 @@ open import Data.Unit.Base             using (⊤)
 open import Data.String.Base as String using (String; _++_; parens)
 open import Data.Product.Base          using (_,_; proj₁)
 open import Function.Base
-open import Relation.Nullary.Decidable
 
 open import Reflection
 open import Reflection.AST.Argument
diff --git a/src/Tactic/RingSolver/NonReflective.agda b/src/Tactic/RingSolver/NonReflective.agda
index cc0b747037..fb33a2b9e0 100644
--- a/src/Tactic/RingSolver/NonReflective.agda
+++ b/src/Tactic/RingSolver/NonReflective.agda
@@ -33,9 +33,7 @@ open import Algebra.Properties.Semiring.Exp.TCOptimised semiring
 
 module Ops where
   zero-homo : ∀ x → T (is-just (0≟ x)) → 0# ≈ x
-  zero-homo x _ with 0≟ x
-  zero-homo x _  | just p = p
-  zero-homo x () | nothing
+  zero-homo x _ with just p ← 0≟ x = p
 
   homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂
   homo = record