`data Elem : a -> List a -> Type`

A proof that some element is found in a list.

**Totality**: total

**Visibility**: public export

**Constructors**:

`Here : Elem x (x :: xs)`

A proof that the element is at the head of the list

`There : Elem x xs -> Elem x (y :: xs)`

A proof that the element is in the tail of the list

**Hints**:

`DecEq (Elem x xs)`

`Injective There`

`Uninhabited (Here = There e)`

`Uninhabited (There e = Here)`

`Uninhabited (Elem x [])`

`Uninhabited (x = z) => Uninhabited (Elem z xs) => Uninhabited (Elem z (x :: xs))`

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

**Totality**: total

**Visibility**: export`isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)`

Check whether the given element is a member of the given list.

**Totality**: total

**Visibility**: public export`get : (xs : List a) -> Elem x xs -> a`

Get the element at the given position.

**Totality**: total

**Visibility**: public export`lookup : (xs : List a) -> Elem x xs -> Singleton x`

Get the element at the given position, with proof that it is the desired element.

**Totality**: total

**Visibility**: public export`dropElem : (xs : List a) -> Elem x xs -> List a`

Remove the element at the given position.

**Totality**: total

**Visibility**: public export`elemToNat : Elem x xs -> Nat`

Erase the indices, returning the numeric position of the element

**Totality**: total

**Visibility**: public export`indexElem : Nat -> (xs : List a) -> Maybe (x : a ** Elem x xs)`

Find the element with a proof at a given position, if it is valid

**Totality**: total

**Visibility**: public export`elemMap : (0 f : (a -> b)) -> Elem x xs -> Elem (f x) (map f xs)`

Lift the membership proof to a mapped list

**Totality**: total

**Visibility**: export