diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -36,7 +36,7 @@
   , vec1, vec2, vec3, vec4, vec5, vec6, vec7, vec8
   , un1, un2, un3, un4
   , get, get0, get1, get2, get3
-  , swizzle, split
+  , swizzle, split, deleteV
   , ToVec(..)
   ) where
 
@@ -551,6 +551,14 @@
 
 -- Could not deduce ((n1 :+: S m) ~ S (n1 :+: m))
 -}
+
+-- | Delete exactly one occurrence of an element from a vector, raising an
+-- error if the element isn't present.
+deleteV :: Eq a => a -> Vec (S n) a -> Vec n a
+deleteV b (a :< as) | a == b = as
+deleteV _ (_ :< ZVec)        = error "deleteV: did not find element"
+deleteV b (a :< as@(_:<_))   = a :< deleteV b as
+
 
 {--------------------------------------------------------------------
     Conversion to vectors
diff --git a/type-unary.cabal b/type-unary.cabal
--- a/type-unary.cabal
+++ b/type-unary.cabal
@@ -1,5 +1,5 @@
 Name:                type-unary
-Version:             0.1.7
+Version:             0.1.8
 Cabal-Version:       >= 1.2
 Synopsis:            
   Type-level and typed unary natural numbers, vectors, inequality proofs