proposition: Lemma in_fset_valP A (p : finmempred _) (k : K) : reflect {kA : k \in A & in_mem [` kA] p} (k \in imfset key val p).
proof: Proof. apply: (iffP (imfsetP _ _ _ _)) => [|[kA xkA]]; last by exists [`kA]. by move=> /sig2_eqW[/= x Xx ->]; exists (valP x); rewrite fsetsubE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)