fact: Definition dom h : pred ptr := nosimpl (if h is Def f _ then mem (supp f) else pred0).
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep