proposition: Lemma size_seq_fset : size (seq_fset s) = size (undup s).
proof: Proof. by rewrite [seq_fset]unlock /= size_sort_keys. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)