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