remove
is defined in a context containing:
Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
The function removes takes this as a first argument (which you can see by doing Print remove.
)
This hypothesis is a function deciding equality of elements of the type in your list. In your case, you will have to provide a function to decide equality of var
(which seems to be nat
, so there is probably such a function in the standard library too).
If you do not know the "{p} + {q}" notation, you can look it up here: http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool