proposition: Lemma alloc_coherent : coherent alloc_sp.
proof: Proof. move=>p x m; split. - case=>i [H1][l][->][->][H2] H3. by exists i; exists H1; exists i; split=>//; exists l. case=>i [H1][_][<-][l][->][->][H2] H3. by exists i; split=>//; exists l. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)