proposition: Lemma val_dealloc (v : A) x i (r : cont unit) : (def i -> r (Val tt) i) -> verify (dealloc_s x) (x :-> v :+ i) r.
proof: Proof. move=>H; apply: val_do; first by [exists A; exists v]; by move=>y m [//][->] ->; rewrite un0h. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)