proposition: Lemma bind_has_spec : bind_sp \In has_spec bind_s.
proof: Proof. move=>i y m. case=>[[[/= S1 S2]]] D [h][x][j][<-][]. case: x=>[x|e] T1; last first. - case=>->->; right; exists e; split=>//. by apply: spec_runs T1. move=>T2; left; exists x; exists j. by split; [apply: spec_runs T1 | apply: spec_runs T2]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)