proposition: Lemma vrfV i (Q : post A) : (valid i -> vrf i e Q) -> vrf i e Q.
proof: Proof. by move=>H V; apply: H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)