proposition: Lemma write_dstrict : def_strict write_sp.
proof: Proof. case=>p H y [i] /= [H1][H2][H3]. suff L: def (upd i x (dyn v)) by move=>H4; rewrite -H4 in L. by rewrite defU (dom_null H2) (dom_def H2). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)