fact: Fixpoint pread x t := match t with Pts y d :: s => if x == y then some d else pread x s | e :: s => pread x s | _ => None end.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)