proposition: Lemma bind_dstrict : def_strict bind_prog.
proof: Proof. move=>i [Vi][Pi P] Vi' y[x][h][/=]. case: x=>[x|e]Ph. - by case=>Ph' /dstr_st. by case=>_; move: Ph=>/[swap]<- /dstr_st. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)