proposition: Lemma ret_mono (v1 v2 : A) : v1 = v2 -> (ret v1 : ST A) <== ret v2.
proof: Proof. by move=>->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)