fact: Definition read_s : spec A := (fun i => x \in dom i /\ exists v:A, look x i = dyn v, fun y i m => m = i /\ forall v, look x i = dyn v -> y = Val v).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)