proposition: Lemma val_doR (s : spec A) h i (r : cont A) (f : Find1 h i) : s.1 i -> (forall x m, s.2 (Val x) i m -> def (m :+ rest1) -> r (Val x) (m :+ rest1)) -> (forall e m, s.2 (Exn e) i m -> def (m :+ rest1) -> r (Exn e) (m :+ rest1)) -> verify s h r.
proof: Proof. move=>H1 H2 H3. generalize (heq1 (h:=h))=>H. rewrite H. by apply: (val_do (i:=i) (j:=rest1)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps stmod stsep stlog)