@@ -573,12 +573,15 @@ implementation DecEq a => DecEq (Vect n a) where
573573||| A proof that some element is found in a vector
574574data Elem : a -> Vect k a -> Type where
575575 Here : Elem x (x::xs)
576− There : Elem x xs -> Elem x (y::xs)
576+ There : (prf : Elem x xs) -> Elem x (y::xs)
577577
578578||| Nothing can be in an empty Vect
579579noEmptyElem : {x : a} -> Elem x [] -> Void
580580noEmptyElem Here impossible
581581
582+Uninhabited (Elem x []) where
583+ uninhabited = noEmptyElem
584+
582585||| An item not in the head and not in the tail is not in the Vect at all
583586neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
584587neitherHereNorThere xneqy xninxs Here = xneqy Refl