proposition: Lemma lookR i t x : def (interp i t) -> has (ptreq x) t -> look (plook' i x) (interp i t) = pread' x t.
proof: Proof. elim: t x=>[//|e1 t IH] x; rewrite interp_cons /=. case F: (ptreq x e1)=>/= D E; last first. - rewrite (lookUnr _ D) (domR (defUnr D) E) (IH _ (defUnr D) E). by case: e1 F {D}=>//= y d ->. case: e1 {E} F D=>// y d; move/eqP=><-{y} D. rewrite (_ : einterp i _ = interp i [:: Pts x d]) // in D *. rewrite (lookUnl _ D) (domR (defUnl D)) /= ?eqxx //. move/defUnl: D=>/=; case: (onth _ x)=>[a|] //. rewrite defPt lookU /= eqxx => ->. by rewrite -dyn_eta. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)