proposition: Lemma fset_sub_pickleK : pcancel fset_sub_pickle fset_sub_unpickle.
proof: Proof. rewrite /fset_sub_unpickle => x. by rewrite (nth_map x) ?nth_index ?index_mem ?mem_fset_sub_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)