proposition: Lemma card_seq_sub : uniq s -> #|{:sT}| = size s.
proof: Proof. by move=> Us; rewrite cardE enumT -(size_map val) unlock val_seq_sub_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)