proposition: Lemma read_coherent : coherent read_sp.
proof: Proof. move=>p v m; split; last first. - by case=>i [H1][<-][w][->]; split=>//; exists w. case=>H1 [w][->] H2. by exists m; exists H1; split=>//; exists w. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)