proposition: Lemma stsp_asym e1 e2 : stsp_leq e1 e2 -> stsp_leq e2 e1 -> e1 = e2.
proof: Proof. move: e1 e2=>[e1 H1][e2 H2]; rewrite /stsp_leq /= =>E1 E2. have E := poset_asym E1 E2; subst e2. by congr STprog; apply: pf_irr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)