fact: Definition app_fsdelta (d : fun_delta K V) f : {fsfun K -> V for default} := [fsfun z in fun_delta_key d |` finsupp f => [eta f with d] z].
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)