proposition: Lemma val_fset_sub_enum : map val fset_sub_enum = enum_fset A.
proof: Proof. rewrite /fset_sub_enum undup_id ?pmap_sub_uniq ?fset_uniq//. rewrite (pmap_filter (@insubK _ _ _)); apply/all_filterP. by apply/allP => x; rewrite isSome_insub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)