diff --git a/src/Util.md b/src/Util.md
index 9264794..7d1342e 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -192,6 +192,14 @@ Lazily generate all the permutations of a Vect
   maxBy f (x :: xs) = Foldable.maxBy f x xs
 ```
 
+### Convert a list to a vect as a sigma type
+
+```idris
+  export
+  listToVect : List a -> (n : Nat ** Vect n a)
+  listToVect xs = (length xs ** fromList xs)
+```
+
 ## Fin
 
 ```idris hide