diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
index 51e2bcf13..c58069d4d 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -2,7 +2,7 @@ module Data.Fin
 
 import public Data.Maybe
 import Data.Nat
-import Decidable.Equality
+import Decidable.Equality.Core
 
 %default total
 
diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index e5cbb1491..e8efc95c8 100644
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@@ -2,6 +2,7 @@ module Data.List
 
 import Data.Nat
 import Data.List1
+import Data.Fin
 
 public export
 isNil : List a -> Bool
@@ -62,6 +63,11 @@ index : (n : Nat) -> (xs : List a) -> {auto 0 ok : InBounds n xs} -> a
 index Z (x :: xs) {ok = InFirst} = x
 index (S k) (_ :: xs) {ok = InLater _} = index k xs
 
+public export
+index' : (xs : List a) -> Fin (length xs) -> a
+index' (x::_)  FZ     = x
+index' (_::xs) (FS i) = index' xs i
+
 ||| Generate a list by repeatedly applying a partial function until exhausted.
 ||| @ f the function to iterate
 ||| @ x the initial value that will be the head of the list