- tailMismatch : Not (this = that) -> Not (There this = There that)
If the tails don't match, neither will references to them.

- 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 List at all

- isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
Is the given element a member of the given list.

- x
The element to be tested.

- xs
The list to be checked against

- intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
The intersectBy function returns the intersect of two lists by user-supplied equality predicate.

- intersect : Eq a => List a -> List a -> List a
Compute the intersection of two lists according to their

`Eq`

implementation.`intersect [1, 2, 3, 4] [2, 4, 6, 8]`

- hereIsNotThere : Not (Here = There later)
`Here`

will never equal`There`

.- dropElem : (xs : List a) -> (p : Elem x xs) -> List a
Remove the element at the given position.

- xs
The list to be removed from

- p
A proof that the element to be removed is in the list

- data Elem : a -> List a -> Type
A proof that some element is found in a list.

Example:

`the (Elem "bar" ["foo", "bar", "baz"]) (tactics { search })`