diff --git a/CHANGELOG.md b/CHANGELOG.md
index cd371e3d8d..22f98d09b7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -341,6 +341,16 @@ Additions to existing modules
   satisfiable⁻ : Satisfiable (Any P) → Satisfiable P
   ```
 
+* In `Data.List.Relation.Unary.First`:
+  ```agda
+  satisfiable    ↦  satisfiable⁺
+  ```
+
+* In `Data.Maybe.Relation.Unary.Any`:
+  ```agda
+  satisfiable    ↦  satisfiable⁺
+  ```
+
 * In `Data.Nat.Divisibility`:
   ```agda
   m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o
@@ -425,6 +435,11 @@ Additions to existing modules
   showAtPrecision : ℕ → ℚᵘ → String
   ```
 
+* In `Data.Tree.AVL.Relation.Indexed.Unary.Any`:
+  ```agda
+  satisfiable    ↦  satisfiable⁺
+  ```
+
 * In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast`:
   ```agda
   castʳ⁺ : Any P lm → Any P (castʳ lm m<u)
@@ -506,6 +521,11 @@ Additions to existing modules
             P kv ⊎ Any P l ⊎ Any P (proj₂ r)
   ```
 
+* In `Data.Tree.AVL.Relation.Unary.Any`:
+  ```agda
+  satisfiable    ↦  satisfiable⁺
+ ```
+
 * In `Data.Vec.Properties`:
   ```agda
   map-removeAt : ∀ (f : A → B) (xs : Vec A (suc n)) (i : Fin (suc n)) →
@@ -560,6 +580,11 @@ Additions to existing modules
                       padRight m≤n x (updateAt xs i f)
   ```
 
+* In `Data.Vec.Relation.Unary.Any`:
+  ```agda
+  satisfiable    ↦  satisfiable⁺
+  ```
+
 * In `Relation.Binary.Construct.Add.Extrema.NonStrict`:
   ```agda
   ≤±-respˡ-≡ : _≤±_ Respectsˡ _≡_
diff --git a/src/Data/List/Relation/Unary/First.agda b/src/Data/List/Relation/Unary/First.agda
index ee0311d527..b418ae33ff 100644
--- a/src/Data/List/Relation/Unary/First.agda
+++ b/src/Data/List/Relation/Unary/First.agda
@@ -78,11 +78,11 @@ module _ {p q} {P : Pred A p} {Q : Pred A q} where
   index-satisfied [ qx ]     = qx
   index-satisfied (_ ∷ pqxs) = index-satisfied pqxs
 
-  satisfied : ∀ {xs} → First P Q xs → ∃ Q
+  satisfied : ∀ {xs} → First P Q xs → Satisfiable Q
   satisfied pqxs = -, index-satisfied pqxs
 
-  satisfiable : Satisfiable Q → Satisfiable (First P Q)
-  satisfiable (x , qx) = List.[ x ] , [ qx ]
+  satisfiable⁺ : Satisfiable Q → Satisfiable (First P Q)
+  satisfiable⁺ (x , qx) = List.[ x ] , [ qx ]
 
 ------------------------------------------------------------------------
 -- Decidability results
@@ -105,3 +105,21 @@ module _ {q} {Q : Pred A q} where
   toAny : ∀ {p} {P : Pred A p} → First P Q ⊆ Any Q
   toAny [ qx ]     = here qx
   toAny (_ ∷ pqxs) = there (toAny pqxs)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+satisfiable = satisfiable⁺
+{-# WARNING_ON_USAGE satisfiable
+"Warning: satisfiable was deprecated in v2.4.
+Please use satisfiable⁺ instead. Moreover,
+the name satisfied will be renamed in v3.0
+to satisfiable, so users should refactor
+as soon as they can."
+#-}
diff --git a/src/Data/Maybe/Relation/Unary/Any.agda b/src/Data/Maybe/Relation/Unary/Any.agda
index b35d033588..2c9f0658f2 100644
--- a/src/Data/Maybe/Relation/Unary/Any.agda
+++ b/src/Data/Maybe/Relation/Unary/Any.agda
@@ -38,7 +38,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where
   map : ∀ {q} {Q : Pred A q} → P ⊆ Q → Any P ⊆ Any Q
   map f (just px) = just (f px)
 
-  satisfied : ∀ {x} → Any P x → ∃ P
+  satisfied : ∀ {x} → Any P x → Satisfiable P
   satisfied (just p) = -, p
 
 ------------------------------------------------------------------------
@@ -72,5 +72,23 @@ module _ {a p} {A : Set a} {P : Pred A p} where
   irrelevant : Irrelevant P → Irrelevant (Any P)
   irrelevant P-irrelevant (just p) (just q) = cong just (P-irrelevant p q)
 
-  satisfiable : Satisfiable P → Satisfiable (Any P)
-  satisfiable P-satisfiable = Product.map just just P-satisfiable
+  satisfiable⁺ : Satisfiable P → Satisfiable (Any P)
+  satisfiable⁺ P-satisfiable = Product.map just just P-satisfiable
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+satisfiable = satisfiable⁺
+{-# WARNING_ON_USAGE satisfiable
+"Warning: satisfiable was deprecated in v2.4.
+Please use satisfiable⁺ instead. Moreover,
+the name satisfied will be renamed in v3.0
+to satisfiable, so users should refactor
+as soon as they can."
+#-}
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index c81599da2a..b215d5b672 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -80,7 +80,7 @@ lookupKey = key ∘′ lookup
 
 -- If any element satisfies P, then P is satisfied.
 
-satisfied : Any P t → ∃ P
+satisfied : Any P t → Satisfiable P
 satisfied (here  p) = -, p
 satisfied (left  p) = satisfied p
 satisfied (right p) = satisfied p
@@ -109,8 +109,26 @@ any? P? (leaf _)          = no λ ()
 any? P? (node kv l r bal) = map′ fromSum toSum
   (P? kv ⊎? any? P? l ⊎? any? P? r)
 
-satisfiable : ∀ {k l u} → l <⁺ [ k ] → [ k ] <⁺ u →
-              Satisfiable (P ∘ (k ,_)) →
-              Satisfiable {A = Tree V l u 1} (Any P)
-satisfiable {k = k} lb ub sat = node (k , proj₁ sat) (leaf lb) (leaf ub) ∼0
-                              , here (proj₂ sat)
+satisfiable⁺ : ∀ {k l u} → l <⁺ [ k ] → [ k ] <⁺ u →
+               Satisfiable (P ∘ (k ,_)) →
+               Satisfiable {A = Tree V l u 1} (Any P)
+satisfiable⁺ {k = k} lb ub sat = node (k , proj₁ sat) (leaf lb) (leaf ub) ∼0
+                               , here (proj₂ sat)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+satisfiable = satisfiable⁺
+{-# WARNING_ON_USAGE satisfiable
+"Warning: satisfiable was deprecated in v2.4.
+Please use satisfiable⁺ instead. Moreover,
+the name satisfied will be renamed in v3.0
+to satisfiable, so users should refactor
+as soon as they can."
+#-}
diff --git a/src/Data/Tree/AVL/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Relation/Unary/Any.agda
index 5efc9363a3..77577708bc 100644
--- a/src/Data/Tree/AVL/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Relation/Unary/Any.agda
@@ -56,9 +56,9 @@ lookup (tree p) = AVLₚ.lookup p
 lookupKey : Any P t → Key
 lookupKey (tree p) = AVLₚ.lookupKey p
 
--- If any element satisfies P, then P is satisfied.
+-- If any element satisfies P, then P is satisfiable.
 
-satisfied : Any P t → ∃ P
+satisfied : Any P t → Satisfiable P
 satisfied (tree p) = AVLₚ.satisfied p
 
 ------------------------------------------------------------------------
@@ -67,6 +67,24 @@ satisfied (tree p) = AVLₚ.satisfied p
 any? : Decidable P → Decidable (Any {V = V} P)
 any? P? (tree p) = map′ tree (λ where (tree p) → p) (AVLₚ.any? P? p)
 
-satisfiable : (k : Key) → Satisfiable (P ∘ (k ,_)) → Satisfiable (Any {V = V} P)
-satisfiable k sat = Product.map tree tree
-                  $ AVLₚ.satisfiable Indexed.⊥⁺<[ k ] Indexed.[ k ]<⊤⁺ sat
+satisfiable⁺ : (k : Key) → Satisfiable (P ∘ (k ,_)) → Satisfiable (Any {V = V} P)
+satisfiable⁺ k sat = Product.map tree tree
+                  $ AVLₚ.satisfiable⁺ Indexed.⊥⁺<[ k ] Indexed.[ k ]<⊤⁺ sat
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+satisfiable = satisfiable⁺
+{-# WARNING_ON_USAGE satisfiable
+"Warning: satisfiable was deprecated in v2.4.
+Please use satisfiable⁺ instead. Moreover,
+the name satisfied will be renamed in v3.0
+to satisfiable, so users should refactor
+as soon as they can."
+#-}
diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda
index 157d275cf9..2b45526a61 100644
--- a/src/Data/Vec/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Relation/Unary/Any.agda
@@ -66,7 +66,7 @@ lookup : Any P xs → A
 lookup {xs = xs} p = Vec.lookup xs (index p)
 
 -- If any element satisfies P, then P is satisfied.
-satisfied : Any P xs → ∃ P
+satisfied : Any P xs → Satisfiable P
 satisfied (here px)   = _ , px
 satisfied (there pxs) = satisfied pxs
 
@@ -77,12 +77,30 @@ any? : Decidable P → ∀ {n} → Decidable (Any P {n})
 any? P? []       = no λ()
 any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎? any? P? xs)
 
-satisfiable : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n})
-satisfiable (x , p) {zero}  = x ∷ [] , here p
-satisfiable (x , p) {suc n} = Product.map (x ∷_) there (satisfiable (x , p))
+satisfiable⁺ : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n})
+satisfiable⁺ (x , p) {zero}  = x ∷ [] , here p
+satisfiable⁺ (x , p) {suc n} = Product.map (x ∷_) there (satisfiable⁺ (x , p))
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
 any = any?
 {-# WARNING_ON_USAGE any
 "Warning: any was deprecated in v1.4.
 Please use any? instead."
 #-}
+
+-- Version 2.4
+
+satisfiable = satisfiable⁺
+{-# WARNING_ON_USAGE satisfiable
+"Warning: satisfiable was deprecated in v2.4.
+Please use satisfiable⁺ instead. Moreover,
+the name satisfied will be renamed in v3.0
+to satisfiable, so users should refactor
+as soon as they can."
+#-}