proposition: Lemma var_has h t : has (vareq h) t = (h \in vars t).
proof: Proof. by elim:t=>[//|e t IH]; case: e=>[//|n]; rewrite /= inE IH. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)