fact: Definition write_prog : prog write_pre unit := fun i _ _ y m => [/\ y = Val tt, m = upd x (idyn v) i & x \in dom i].
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)