Spot the difference

elemimp.idr

  data Elem : a -> Vect n a -> Type where
       Here : Elem x (x :: xs)
       There : Elem x xs -> Elem x (y :: xs)
  
  isElem : DecEq a => (x : a) -> (xs : _) -> Maybe (Elem x xs)
  isElem x [] = Nothing
  isElem x (y :: xs) with (decEq x y)
    isElem x (x :: xs) | (Yes refl) = Just Here
    isElem x (y :: xs) | (No contra) = Just (There !(isElem x xs))