fact: Example ex_val_do (s : spec nat) (r : cont nat) (x y : ptr) : s.1 (y:->2) -> (forall x' m, s.2 (Val x') (y:->2) m -> def (x:->1:+m) -> r (Val x') (x:->1:+m)) -> (forall e m, s.2 (Exn e) (y:->2) m -> def (x:->1:+m) -> r (Exn e) (x:->1:+m)) -> verify s (x:->1 :+ y:->2) r.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps stmod stsep stlog)