proposition: Lemma restrictf0 f : f.[& fset0] = [fmap].
proof: Proof. by apply/fmapP => k; rewrite fnd_restrict !(inE, not_fnd). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)