proposition: Lemma bind_dstrict : def_strict bind_sp.
proof: Proof. move=>p y [i][x][h][H1][]. case: x=>[x'|e] H2; first by case/def_runs. by case=>_ E; case/def_runs: H2; rewrite -E. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)