fact: Definition pre_sup (u : Pred ST) : pre := fun h => forall e, e \In u -> h \In pre_of e.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)