Show that index (∈-lookup i xs) is in fact i (#1264)

Author: umazalakain

CHANGELOG.md

@@ -506,6 +506,11 @@ Other minor additions
   take⁺ : ∀ {n} m {xs} → All P {m + n} xs → All P {m} (take m xs)
   ```
 
+* Added new proofs to `Data.Vec.Membership.Propositional.Properties`:
+  ```agda
+  index-∈-lookup : (i : Fin n) (xs : Vec A n) → Any.index (∈-lookup i xs) ≡ i
+  ```
+
 Refactorings
 ------------
 

src/Data/Vec/Membership/Propositional/Properties.agda

@@ -14,14 +14,14 @@ open import Data.Vec hiding (here; there)
 open import Data.Vec.Relation.Unary.Any using (here; there)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
-open import Data.Vec.Relation.Unary.Any using (Any; here; there)
+open import Data.Vec.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Vec.Membership.Propositional
 open import Data.List.Membership.Propositional
   using () renaming (_∈_ to _∈ₗ_)
 open import Level using (Level)
 open import Function using (_∘_; id)
 open import Relation.Unary using (Pred)
-open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
 
 private
   variable
@@ -36,6 +36,10 @@ private
 ∈-lookup zero    (x ∷ xs) = here refl
 ∈-lookup (suc i) (x ∷ xs) = there (∈-lookup i xs)
 
+index-∈-lookup : ∀ {n} (i : Fin n) (xs : Vec A n) → Any.index (∈-lookup i xs) ≡ i
+index-∈-lookup zero (x ∷ xs) = refl
+index-∈-lookup (suc i) (x ∷ xs) = cong suc (index-∈-lookup i xs)
+
 ------------------------------------------------------------------------
 -- map