proposition: Lemma val_ghR (r : cont A) : let: s := (fun i => exists x, i \In p x, fun y i m => forall x, i \In p x -> q x y i m) in (forall x m, q t (Val x) i m -> def (f m) -> r (Val x) (f m)) -> (forall e m, q t (Exn e) i m -> def (f m) -> r (Exn e) (f m)) -> i \In p t -> verify s (f i) r.
proof: Proof. move=>H1 H2; rewrite updateE; apply: val_gh. - by move=>x m; move: (H1 x m); rewrite updateE. by move=>x m; move: (H2 x m); rewrite updateE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)