proposition: Lemma fsfun_ffun (S : {fset K}) (h : S -> V) (x : K) : [fsfun[key] a : S => h a | default a] x = odflt (default x) (omap h (insub x)).
proof: Proof. by rewrite unlock. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)