proposition: Lemma hstep A i (r : post A) p (e : val_form i r p) : p -> vrf i e r.
proof: Proof. by case:e=>[?]; apply. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)