proposition: Lemma vars_hfree (h1 h2 : nat) t : has (vareq h1) (hfree h2 t) = (h1 != h2) && (has (vareq h1) t).
proof: Proof. elim:t=>[|e t IH]; first by rewrite andbF. case: e=>[//|n /=]. by case: ifP=>/= E; rewrite IH; case: (h1 =P n)=>// ->; rewrite eq_sym E. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)