Idris2Doc : Data.List.Elem.Extra

Data.List.Elem.Extra

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