proposition: Lemma heap_eta x h : x \in dom h -> exists A (v : A), find x h = Some (idyn v) /\ h = x :-> v \+ free h x.
proof: Proof. by case/um_eta; case=>A v H; exists A, v. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)