- replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
- replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t
- overLength : (len : Nat) -> (xs : Vect m a) -> Maybe (p : Nat ** Vect (plus p len) a)
If the given Vect is at least the required length, return a Vect with

at least that length in its type, otherwise return Nothing- len
the required length

- xs
the vector with the desired length

- noEmptyElem : Elem x [] -> Void
Nothing can be in an empty Vect

- neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
An item not in the head and not in the tail is not in the Vect at all

- mapElem : Elem x xs -> Elem (f x) (map f xs)
- isLength : (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
If the given Vect is the required length, return a Vect with that

length in its type, otherwise return Nothing- len
the required length

- xs
the vector with the desired length

- isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
A decision procedure for Elem

- findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic
A tactic for discovering where, if anywhere, an element is in a vector

- n
how many elements to search before giving up

- data Elem : a -> Vect k a -> Type
A proof that some element is found in a vector