proposition: Lemma stsp_supM u e : (forall e1, e1 \In u -> e1 <== e) -> stsp_sup u <== e.
proof: Proof. by case: e=>p S R; apply: supM=>/= y[q][->]; apply: R. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)