From ea6aad0e25358e3a249c5bf3401c0238805cf85c Mon Sep 17 00:00:00 2001
From: 0xd34df00d <0xd34df00d@gmail.com>
Date: Sun, 8 Oct 2023 15:11:30 -0500
Subject: [PATCH] [ base ] Prove `anyToFin` preserves the property witnessed by
 `Any`

---
 libs/base/Data/Vect/Quantifiers.idr | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/libs/base/Data/Vect/Quantifiers.idr b/libs/base/Data/Vect/Quantifiers.idr
index 574b146ab2..6157bb27df 100644
--- a/libs/base/Data/Vect/Quantifiers.idr
+++ b/libs/base/Data/Vect/Quantifiers.idr
@@ -67,6 +67,14 @@ namespace Any
   anyToFin (Here _) = FZ
   anyToFin (There later) = FS (anyToFin later)
 
+  ||| `anyToFin`'s return type satisfies the predicate
+  export
+  anyToFinCorrect : {0 xs : Vect n a} ->
+                    (witness : Any p xs) ->
+                    p (anyToFin witness `index` xs)
+  anyToFinCorrect (Here prf) = prf
+  anyToFinCorrect (There later) = anyToFinCorrect 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`.