proposition: Lemma st_supM (u : Pred ST) e : (forall e1, e1 \In u -> st_leq e1 e) -> st_leq (st_sup u) e.
proof: Proof. by case: e=>p M S H R; apply: supM=>y [q][->]; apply: R. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)