fact: Definition do_sp (p : ideald s2.1) y m := exists i, i \In id_val p /\ (i, y, m) \In runs_of (model e).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)