proposition: Lemma stsp_supP u e : e \In u -> e <== stsp_sup u.
proof: Proof. by case: e=>p S R; apply: supP; exists (STprog S). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)