proposition: Lemma defR i t : def (interp i t) -> uniq (ptrs t).
proof: Proof. elim: t=>[//|e t IH]; rewrite interp_cons /=. case: e=>[y d|n] /=; case E: (onth _ _)=>[a|//]; last by move/defUnr. case: defUn=>// D1 D2 L _. rewrite (IH D2) andbT -ptr_has. apply: contra (L a _); first by move/(domR D2); rewrite /= E. by rewrite defPt domPt !inE eqxx in D1 *. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)