proposition: Lemma hfree_subdom i h t : def (interp i t) -> {subset dom (interp i (hfree h t)) <= dom (interp i t)}.
proof: Proof. elim:t=>[_ x //|e t IH]; rewrite interp_cons /= => D. case: ifP=>_; last first. - move=>x; move/(IH (defUnr D)). by rewrite domUn !inE D orbC => ->. rewrite interp_cons => x; rewrite !domUn !inE D /=. case/andP=>D2; case/orP; rewrite ?inE; first by move->. by move/(IH (defUnr D) x)=>->; rewrite orbT. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)