proposition: Lemma do_has_spec : do_sp \In has_spec s2.
proof: Proof. move=>i y m [[/= S1 D1]][_][<-] T; case/def_runs: (T)=>_ S2 D2. by apply: (proj2 (pf S1 D1)) D2; apply: spec_runs T. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)