Data.List.Elem.Extra

Definitions

elemAppLeft : (xs : List a) -> (ys : List a) -> Elem x xs -> Elem x (xs ++ ys)

  Proof that an element is still inside a list if we append to it.

Totality: total
Visibility: public export

elemAppRight : (ys : List a) -> (xs : List a) -> Elem x xs -> Elem x (ys ++ xs)

  Proof that an element is still inside a list if we prepend to it.

Totality: total
Visibility: public export

elemAppLorR : (xs : List a) -> (ys : List a) -> Elem k (xs ++ ys) -> Either (Elem k xs) (Elem k ys)

  Proof that membership on append implies membership in left or right sublist.

Totality: total
Visibility: public export

notElemAppLeft : (xs : List a) -> (ys : List a) -> Not (Elem x (xs ++ ys)) -> Not (Elem x xs)

  Proof that x is not in (xs ++ ys) implies proof that x is not in xs.

Totality: total
Visibility: public export

notElemAppRight : (ys : List a) -> (xs : List a) -> Not (Elem x (xs ++ ys)) -> Not (Elem x ys)

  Proof that x is not in (xs ++ ys) implies proof that x is not in ys.

Totality: total
Visibility: public export