proposition: Lemma ptr_has x t : has (ptreq x) t = (x \in ptrs t).
proof: Proof. by elim:t=>[//|e t IH]; case: e=>[y d|//]; rewrite /= inE IH. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)