proposition: Lemma val_alloc (v : A) i (r : cont ptr) : (forall x, def (x :-> v :+ i) -> r (Val x) (x :-> v :+ i)) -> verify (alloc_s v) i r.
proof: Proof. move=>H; rewrite -[i]un0h; apply: val_do=>//; by move=>y m [x][//][-> ->]; apply: H. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)