diff --git a/CHANGELOG.md b/CHANGELOG.md
index e951804d71..629d5c569e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -186,6 +186,9 @@
 
 * Add `zipPropertyWith` to `Data.Vect.Quantifiers.All.All`.
 
+* Add `anyToFin` to `Data.Vect.Quantifiers.Any`,
+  converting the `Any` witness to the index into the corresponding element.
+
 * Implemented `Ord` for `Language.Reflection.TT.Name`, `Language.Reflection.TT.Namespace`
   and `Language.Reflection.TT.UserName`.
 
diff --git a/libs/base/Data/Vect/Quantifiers.idr b/libs/base/Data/Vect/Quantifiers.idr
index 7ee5ca0200..574b146ab2 100644
--- a/libs/base/Data/Vect/Quantifiers.idr
+++ b/libs/base/Data/Vect/Quantifiers.idr
@@ -61,6 +61,12 @@ namespace Any
   toExists (Here prf)  = Evidence _ prf
   toExists (There prf) = toExists prf
 
+  ||| Get the bounded numeric position of the element satisfying the predicate
+  public export
+  anyToFin : {0 xs : Vect n a} -> Any p xs -> Fin n
+  anyToFin (Here _) = FZ
+  anyToFin (There later) = FS (anyToFin later)
+
 namespace All
   ||| A proof that all elements of a vector satisfy a property. It is a list of
   ||| proofs, corresponding element-wise to the `Vect`.