fact: Definition assocs h : seq (ptr_ordType * dynamic id) := if h is Def f _ then seq_of f else [::].
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)