proposition: Lemma getfP V (f g : {fmap K -> V}) : domf f = domf g -> (forall k (kMf : k \in f) (kMg : k \in g), f.[kMf] = g.[kMg]) -> f = g.
proof: Proof. move: f g => [kf f] [kg g] /= eq_kfg; case: _ / eq_kfg in g * => {kg}. move=> eq_fg; congr FinMap; apply/ffunP => /= x. by do [rewrite -!getfE; do ?exact: valP] => *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)