fact: Definition st_sup u : ST := Prog (@pre_sup_sfmono u) (@prog_sup_dstrict u) (@prog_sup_frame u).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)