proposition: Lemma throw_mono (e1 e2 : exn) : e1 = e2 -> (throw A e1 : ST A) <== throw A e2.
proof: Proof. by move=>->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)