proposition: Lemma val_gh (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 (m :+ j) -> r (Val x) (m :+ j)) -> (forall e m, q t (Exn e) i m -> def (m :+ j) -> r (Exn e) (m :+ j)) -> i \In p t -> verify s (i :+ j) r.
proof: Proof. by move=>*; apply: val_do=>/=; eauto. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)