proposition: Lemma allocP : Model.conseq (Model.alloc_s v) [alloc_s].
proof: Proof. move=>i H D; split=>[|{H D} y m [x][H1][->][H2] <- D1 i1 h E1 D E2]. - by case: H D=>i1 [i2][->][->]. move: E1 E2 H2 D D1=>-> ->; rewrite {1 2}un0h=>H2 D D1. exists (x :-> v); rewrite updUnr (negbTE H2) defPtUn H1 H2 D. by do !split=>//; exists x. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)