proposition: Lemma fset_sub_val A (p : finmempred A) : (imfset key val p) `<=` A.
proof: Proof. by apply/fsubsetP => k /in_fset_valP []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)