proposition: Lemma bind_mono (e1 e2 : ST A) (k1 k2 : A -> ST B) : e1 <== e2 -> k1 <== k2 -> (bind e1 k1 : ST B) <== bind e2 k2.
proof: Proof. move=>[H1 H2] pf2. have pf: bind_pre e2 k2 <== bind_pre e1 k1. - move=>h [Vh][Pi] H. exists Vh, (H1 _ Pi)=>x m /H2/H H'. by case: (pf2 x)=>+ _; apply. exists pf=>i Vi /[dup][[Vi'][Pi']P'] Pi x h. case; case=>[a|e][h0][Ph][Ph'] H. - exists (Val a), h0. move: (H2 i Vi (bind_pre_proj Pi))=>H'. rewrite (pf_irr (H1 i (bind_pre_proj Pi)) (bind_pre_proj (pf i Pi))) in H'. have Ph0 := (H' _ _ Ph); exists Ph0. move: (P' a h0); rewrite (pf_irr Vi' Vi) (pf_irr Pi' (bind_pre_proj Pi))=>H''. exists (H'' Ph0); case: (pf2 a)=>Pr; apply. by rewrite (pf_irr (dstr_valid Ph0) (dstr_valid Ph)) (pf_irr (Pr h0 (H'' Ph0)) Ph'). rewrite Ph' H; exists (Exn e), h0. move: (H2 i Vi (bind_pre_proj Pi))=>H'. rewrite (pf_irr (H1 i (bind_pre_proj Pi)) (bind_pre_proj (pf i Pi))) in H'. by exists (H' _ _ Ph). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)