proposition: Lemma st_sup_dstrict u : def_strict (st_sup' u).
proof: Proof. by move=>p x [_][[_]][[_]][[_]][[]][r] M D H [->] P -> -> -> /=; move/D. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)