- 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]`

- 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 })`