Idris2Doc : Data.List.Elem.Extra

Data.List.Elem.Extra

Definitions

elemAppLeft : (xs : Lista) -> (ys : Lista) ->Elemxxs->Elemx (xs++ys)
  Proof that an element is still inside a list if we append to it.

Totality: total
Visibility: public export
elemAppRight : (ys : Lista) -> (xs : Lista) ->Elemxxs->Elemx (ys++xs)
  Proof that an element is still inside a list if we prepend to it.

Totality: total
Visibility: public export
elemAppLorR : (xs : Lista) -> (ys : Lista) ->Elemk (xs++ys) ->Either (Elemkxs) (Elemkys)
  Proof that membership on append implies membership in left or right sublist.

Totality: total
Visibility: public export
notElemAppLeft : (xs : Lista) -> (ys : Lista) ->Not (Elemx (xs++ys)) ->Not (Elemxxs)
  Proof that x is not in (xs ++ ys) implies proof that x is not in xs.

Totality: total
Visibility: public export
notElemAppRight : (ys : Lista) -> (xs : Lista) ->Not (Elemx (xs++ys)) ->Not (Elemxys)
  Proof that x is not in (xs ++ ys) implies proof that x is not in ys.

Totality: total
Visibility: public export