fact: Fixpoint ptrs t : seq nat := if t is e :: t' then if e is Pts x _ then x :: (ptrs t') else ptrs t' else [::].
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)