proposition: Lemma empty_hfree i v t : hlook i v = Some empty -> interp i (hfree v t) = interp i t.
proof: Proof. elim: t=>[//|[x d|v'] t IH] H1; rewrite [hfree _ _]/=. - by rewrite 2!interp_cons IH. case: ifP=>H2; first by rewrite 2!interp_cons IH. rewrite /= in H1; rewrite -(eqP (negbFE H2)) {}IH //= H1. by case: t=>[//|e s]; rewrite un0h. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)