proposition: Lemma val_allocb (v : A) n i (r : cont ptr) : (forall x, def (updi x (nseq n v) :+ i) -> r (Val x) (updi x (nseq n v) :+ i)) -> verify (allocb_s v n) 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)