proposition: Lemma vrf_post i (Q1 Q2 : post A) : (forall y m, valid m -> Q1 y m -> Q2 y m) -> vrf i e Q1 -> vrf i e Q2.
proof: Proof. move=>H H1 Vi; case: (H1 Vi)=>pf {}H1. exists pf=>y m Hm. by apply/H/H1=>//; exact: (dstr_valid Hm). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)