fact: Definition fsfun_of_ffun key (K : choiceType) (V : eqType) (S : {fset K}) (h : S -> V) (default : K -> V) := (Fsfun.of_ffun default h key).
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)