proposition: Lemma count1_hfree v t : count (pred1 v) (vars t) = 1 -> perm (Var v :: hfree v t) t.
proof: Proof. elim: t=>[//|w t IH]; case: w=>[x d H|v'] /=. - rewrite perm_sym -(cat1s (Var v) _). apply: perm_cons_cat_consL. by rewrite perm_sym; apply: IH. rewrite eq_sym; case: eqP=>[->|_] /=. rewrite -{2}[1]addn0; move/eqP; rewrite eqn_add2l; move/eqP. by move/count0_hfree=>->. rewrite add0n; move/IH=>H; rewrite perm_sym -(cat1s (Var v)). by apply: perm_cons_cat_consL; rewrite perm_sym. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)