proposition: Lemma pfree_def i x t: def (interp i t) -> def (interp i (pfree x t)).
proof: Proof. by move/(pfree_subdom x); move/subdom_def; move/andP=>[-> _]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)