proposition: Lemma domR i (x : nat) t : def (interp i t) -> has (ptreq x) t -> plook' i x \in dom (interp i t).
proof: Proof. elim: t x=>[//|e1 t IH] x; rewrite interp_cons /= => D. case/orP=>E; last by rewrite domUn !inE D (IH _ (defUnr D) E) orbT. rewrite domUn !inE D. case: e1 E D=>//= y d; move/eqP=><-; move/defUnl. case: (onth _ _)=>[a|] //=. by rewrite defPt domPt !inE eqxx => ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)