fact: Definition st_sup' (u : Pred STspec) : ST A := sup [Pred p | exists e, p = model e /\ e \In u].
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)