proposition: Lemma deallocP : Model.conseq (Model.dealloc_s x) [dealloc_s].
proof: Proof. move=>i H D; split=>[|{H D} y m [->] <- D1 i1 h E1 D2 [A][v] E2]. - case: H D=>i1 [i2][->][[A]][v]-> _ D /=. by rewrite domPtUn inE /= D eq_refl. move: E1 E2 D1 D2=>->->->; rewrite defPtUn; case/and3P=>H1 _ H2. by exists empty; rewrite freeUnr // freeU eq_refl (negbTE H1) free0. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)