proposition: Lemma val_do (s : spec A) i j (r : cont A) : s.1 i -> (forall x m, s.2 (Val x) i m -> def (m :+ j) -> r (Val x) (m :+ j)) -> (forall e m, s.2 (Exn e) i m -> def (m :+ j) -> r (Exn e) (m :+ j)) -> verify s (i :+ j) r.
proof: Proof. move=>H1 H2 H3; apply: frame; apply: frame0; split=>//. by case=>x m H4 D1 D2; [apply: H2 | apply: H3]. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)