fact: Definition st_leq e1 e2 := exists pf : pre_of e2 <== pre_of e1, forall i (v : valid i) (p : i \In pre_of e2), prog_of e1 _ v (pf _ p) <== prog_of e2 _ v p.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)