proposition: Lemma ghE (B : Type) (q : heap -> B -> Prop) (r : B -> post A) : (forall i, p i -> def i -> exists x, q i x) -> (forall i x, q i x -> p i -> def i -> verify s i (fun y m => r x y i m)) -> conseq s p (fun y i m => forall x, q i x -> r x y i m).
proof: Proof. move=>H1 H2 i H3 D1; case: (H1 i H3 D1)=>x H4. case: (H2 i x H4 H3 D1 D1)=>H5 _; split=>// y m H6 D2 z H7. by case: (H2 i z H7 H3 D1 D1)=>_; apply. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)