proposition: Lemma count0_hfree v t: count (pred1 v) (vars t) = 0 -> hfree v t = t.
proof: Proof. by move/eqP; rewrite eqn0Ngt -has_count has_pred1; apply: hfreeN. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)