Check that a list contains an element

-- Proof of the fact that list contains an element
data Contains : a -> List a -> Type where
  Here : (x : a) -> (xs : List a) -> Contains x (x :: xs)
  There : (x : a) -> Contains y xs -> Contains y (x :: xs)

-- Check that list contains an element and return a proof
total list_contains : DecEq a => (x : a) -> (xs : List a) -> Dec (Contains x xs)

Please log in; otherwise your solution and progress won't be saved