proposition: Lemma hfree_def i h t : def (interp i t) -> def (interp i (hfree h t)).
proof: Proof. by move/(hfree_subdom' h); move/subdom_def; move/andP=>[-> _]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)