fact: Definition write_s : spec unit := (fun i => exists B : Type, exists y : B, i = x :-> y, fun y i m => y = Val tt /\ m = x :-> v).
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)