proposition: Lemma write_coherent : coherent write_sp.
proof: Proof. move=>p y m; split; case=>i [H1]. - by case=>H2 [->->]; exists i; exists H1; exists i. by case=>_ [<-][H2][->] ->; exists i. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)