proposition: Lemma pfreeN x t : x \notin ptrs t -> pfree x t = t.
proof: Proof. rewrite -ptr_has; elim: t=>[|e t IH] //=; rewrite negb_or. by case/andP=>->; move/IH=>->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)