proposition: Lemma fmap_nil V (f : {fmap K -> V}) : domf f = fset0 -> f = [fmap].
proof: Proof. by move=> kf0; apply: getfP => //= k ? kMg; have := kMg; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)