proposition: Lemma st_supP (u : Pred ST) e : e \In u -> st_leq e (st_sup u).
proof: Proof. by case: e=>p M S H R; apply: supP; exists (STprog M S H). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)