fact: Definition read_pre : pre := fun i => x \in dom i /\ exists v : A, find x i = Some (idyn v).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)