fact: Structure STspec G A (s : spec G A) := STprog { model :> ST A; _ : model \In has_spec s}.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)