proposition: Lemma st_refl e : st_leq e e.
proof: Proof. exists (poset_refl _)=>i V P y m. by rewrite (pf_irr (poset_refl (pre_of e) i P) P). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)