proposition: Lemma in_fset_val A (p : finmempred A) (k : K) : (k \in imfset key val p) = if insub k is Some a then in_mem a p else false.
proof: Proof. have [a _ <- /=|kNA] := insubP; first by rewrite val_in_fset. by apply/imfsetP => [] [a _ k_def]; move: kNA; rewrite k_def [_ \in _]valP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)