fact: Definition einterp i e := match e with Pts x d => if plook i x is Some x' then x' :-> Dyn.val d else Undef | Var h => if hlook i h is Some h' then h' else Undef end.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)