proposition: Lemma allocbP : Model.conseq (Model.allocb_s v n) [allocb_s].
proof: Proof. move=>i H D; split=>[|y m]. by case: H D=>i1 [i2][->][->][]; rewrite unC. case=>x [->] -> D1 i1 h E1 D2 E2. move: E1 E2 D1 D2=>->->; rewrite un0h {2}unC=>D1 D2. by exists (updi x (nseq n v)); do !split=>//; exists x. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)