proposition: Lemma frame i j (r : ans A -> heap -> Prop) : verify s i (fun y m => def (m :+ j) -> r y (m :+ j)) -> verify s (i :+ j) r.
proof: Proof. move=>H D; case: (H (defUnl D))=>H1 H2. split=>[|y m]; first by apply: fr_pre. case/(locality D H1)=>m1 [->][D1]; move/H2. by apply; apply: defUnl D1. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)