fact: Definition fsfun_of_fun key (K : choiceType) (V : eqType) (S : {fset K}) (h : K -> V) default := [fsfun[key] x : S => h (val x) | default x].
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)