proposition: Lemma frame1 i (r : ans A -> heap -> Prop) : verify' s empty (fun y m => def (m :+ i) -> r y (m :+ i)) -> verify s i r.
proof: Proof. by move=>H; rewrite -[i]un0h; apply: frame; apply: frame0. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)