proposition: Lemma size_of_uniq (T0 : choiceType) (s : seq T0) : uniq s -> size (set_of s) = size s.
proof: Proof. move/set_of_uniq. exact: perm_size. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)