fact: Definition write_sp (p : ideald write_s.1) (y : ans unit) m := exists i, i \In id_val p /\ x \in dom i /\ y = Val tt /\ m = upd i x (dyn v).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)