proposition: Lemma st_asym e1 e2 : st_leq e1 e2 -> st_leq e2 e1 -> e1 = e2.
proof: Proof. move: e1 e2=>[e1 M1 S1 H1][e2 M2 S2 H2]; rewrite /st_leq /= => E1 E2. rewrite (poset_asym E1 E2) in M1 M2 S1 S2 H1 H2 *; congr STprog; by apply: proof_irrelevance. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)