proposition: Lemma st_sup_has_spec u : st_sup' u \In has_spec s.
proof: Proof. move=>i y m [/= D]. case=>_ [[_]][[_]][[_]][[]][p] M S H [->] P -> -> -> /= R. by apply: (H); exists D. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)