proposition: Lemma in_fset_valF A (p : finmempred A) (k : K) : k \notin A -> (k \in imfset key val p) = false.
proof: Proof. by apply: contraNF => /imfsetP[/= a Xa->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)