proposition: Lemma stsp_refl e : stsp_leq e e.
proof: Proof. by case: e=>e He; apply: poset_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)