fact: Definition look (x : ptr) h := (if h is Def hs _ then if fnd x hs is Some d then d else dyn tt else dyn tt).
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep