proposition: Lemma freeR i t x : def (interp i t) -> has (ptreq x) t -> free (plook' i x) (interp i t) = interp i (pfree x t).
proof: Proof. elim: t=>[//|e t IH]; rewrite interp_cons=>D /=. case E: (ptreq x e)=>/=; last first. - move=>H; rewrite freeUnl; first by rewrite (IH (defUnr D) H) -{1}interp_cons. case: defUn D=>// D1 D2 L _. apply: (contra (L (plook' i x))); rewrite negbK. by apply: domR. case: e E D=>//= y d; move/eqP=><-{y}. case F: (onth _ x)=>[a|//] D _. rewrite freePtUn //= pfreeN // -ptr_has. apply: contra (defPt_dom D); move/(domR (defPt_def D)). by rewrite /= F. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)