proposition: Lemma do_mono G (e1 e2 : ST A) (s : spec G A) (pf1 : has_spec s e1) (pf2 : has_spec s e2) : e1 <== e2 -> @STprog _ _ _ e1 pf1 <== @STprog _ _ _ e2 pf2.
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)