proposition: Lemma heap_eta2 A x h (v : A) : find x h = Some (idyn v) -> h = x :-> v \+ free h x.
proof: Proof. move=>E; case: (heap_eta (find_some E))=>B [w][]. rewrite {}E; case=>E; rewrite -E in w *. by move/(@inj_pair2 _ _ _ _ _)=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)