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