proposition: Lemma read_has_spec : read_sp \In has_spec read_s.
proof: Proof. move=>i y m [[[/= H1]]][v] H2 D [<-][w][->] H3. by split=>// b1; rewrite H3=>H; move:(dyn_inj H)=>->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)