proposition: Lemma hfreeN h t : h \notin vars t -> hfree h t = t.
proof: Proof. rewrite -var_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)