proposition: Lemma st_bot_has_spec : @st_bot A \In has_spec.
proof: Proof. by move=>g i H V /=; exists I. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)