proposition: Lemma allocb_dstrict : def_strict allocb_sp.
proof: Proof. case=>p H y [m][/= H1][_] H2; case/H: H1=>_ D. suff {H2}: def (m :+ updi (fresh m) (nseq n v)) by rewrite -H2. elim: n =>[|k IH]; first by rewrite /= unh0. rewrite (_ : nseq k.+1 v = rcons (nseq k v) v); last first. - by elim: {IH} k=>[|k IH] //=; rewrite -IH. rewrite updi_last unA unC defPtUn IH /=. rewrite ptr_null negb_and fresh_null /=. rewrite domUn !inE /= negb_and IH negb_or /=. by rewrite dom_fresh updimV negb_and fresh_null ltnn. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)