proposition: Lemma frame0 i r : verify' s i r -> verify s i r.
proof: Proof. move=>H D; case: (H D)=>H1 H2. split=>[|y m]; first by exists i; exists empty; rewrite unh0. move/(_ i empty); rewrite unh0; case/(_ (erefl _) D H1)=>m1. by rewrite unh0=>[[<-]][_]; apply: H2. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)