proposition: Lemma in_fset_valT A (p : finmempred _) (k : K) (kA : k \in A) : (k \in imfset key val p) = in_mem [` kA] p.
proof: Proof. by rewrite in_fset_val insubT /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)