proposition: Lemma st_supP u e : e \In u -> e <== st_sup u.
proof: Proof. case: e=>p e' S D F R. exists (pre_sup_leq R)=>/=p0 y m H. by exists (Prog S D F), R. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)