proposition: Lemma hfreeE h t : hfree h t = if t is e :: t' then if e is Var k then if h == k then hfree h t' else e :: hfree h t' else e :: hfree h t' else [::].
proof: Proof. by elim:t=>[|e t IH] //; case: e=>[| n] //=; case: eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)