proposition: Lemma hfree_subdom' i h t : def (interp i t) -> subdom (interp i (hfree h t)) (interp i t).
proof: Proof. elim:t=>[//|e t IH]; rewrite interp_cons /= => D. case: ifP=>_; last first. - rewrite -(un0h (interp _ _)). apply: subdomUE=>//. - by apply: subdom_emp; rewrite (defUnl D). by apply: IH; rewrite (defUnr D). rewrite interp_cons. apply: subdomUE=>//. - by apply: subdom_refl; rewrite (defUnl D). by apply: IH; rewrite (defUnr D). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)