import Data.Vect {- data Elem : a -> Vect k a -> Type where Here : Elem x (x :: xs) There : (later : Elem x xs) -> Elem x (y :: xs) -} total removeElem : (value : a) -> (xs : Vect (S n) a) -> (witn : Elem value xs) -> Vect n a removeElem value (value :: ys) Here = ys {- removeElem value (y :: []) (There later) = absurd later -} removeElem {n = (S k)} value (y :: ys) (There later) = y :: removeElem value ys later not_in_nil : Elem value [] -> Void not_in_nil Here impossible not_in_nil (There _) impossible