fact: Definition has_spec A (s : spec A) := [Pred c : prog A s.1 | forall i y m, (i, y, m) \In runs_of c -> s.2 y i m].
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)