proposition: Lemma read_dstrict : def_strict read_prog.
proof: Proof. by move=>i _ Vi _ [_ [E _ _]]; rewrite -E in Vi. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)