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