proposition: Lemma fsfun_of_can_ffunE (T : {fset K}) (g : {ffun T -> V}) (can_g : forall k : T , g k != default (val k)) k (kg : k \in T) : (fsfun_of_can_ffun can_g) k = g.[kg].
proof: Proof. by rewrite/fun_of_fsfun in_fnd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)