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

**Totality**: total

**Visibility**: public export Proof that an element is still inside a list if we prepend to it.

**Totality**: total

**Visibility**: public export Proof that membership on append implies membership in left or right sublist.

**Totality**: total

**Visibility**: public export Proof that x is not in (xs ++ ys) implies proof that x is not in xs.

**Totality**: total

**Visibility**: public export Proof that x is not in (xs ++ ys) implies proof that x is not in ys.

**Totality**: total

**Visibility**: public export