proposition: Corollary vrf_mono A (e : ST A) i : monotone (vrf' e i).
proof: Proof. by move=>/= Q1 Q2 H; apply: vrf_post=>y m _; apply: H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)