proposition: Corollary dstr_valid e i p v x m : m \In prog_of e i p v x -> valid m.
proof: Proof. by case: m=>// /dstr_st. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)