fact: Definition assocs f : seq (K * V) := if f is Def fs _ then seq_of fs else [::].
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)