fact: Definition alloc_s : spec ptr := (fun i => def i : Prop, fun y i m => exists x, x != null /\ y = Val x /\ x \notin dom i /\ upd i x (dyn v) = m).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)