proposition: Lemma heap_etaP h x : x \in dom h -> h = x :-> Dyn.val (look x h) :+ free x h.
proof: Proof. move=>H; rewrite {1}(heap_eta H) /pts -dyn_eta. by rewrite -{1}[free x h]un0h updUnr domF inE /= eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep