proposition: Lemma pfreeE x t : pfree x t = if t is e :: t' then if e is Pts y d then if x == y then pfree x t' else e :: pfree x t' else e :: pfree x t' else [::].
proof: Proof. by elim:t=>[|e t IH] //; case: e=>[y d|] //=; case: eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)