fact: Definition seq_fset : forall K : choiceType, seq K -> {fset K} := locked_with finset_key (fun K s => mkFinSet (@canonical_sort_keys K s)).
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)