proposition: Lemma bnd_case_pf A B i (s : A -> ST B) r p (e : bnd_form i s r p) : p -> vrf i (bind e s) r.
proof: Proof. by case:e=>[?]; apply. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)