proposition: Lemma tseq_uniq : uniq tseq.
proof: Proof. rewrite /tseq -(revK (enum T)) foldl_rev. have uniqrevl: uniq (rev (enum T)) by rewrite rev_uniq; apply: enum_uniq. elim: rev uniqrevl => //= x l IH /andP. case fld: (foldr _ _ _) => [s l'] [xl uniql]. have uniq0: @uniq T [::] by []. have sub0: {subset [::] <= ~: [set: T]} by []. have [uniql' subs] := foldr_pdfs_subset uniq0 sub0 fld. exact: pdfs_uniq. Qed.
imports: mathcomp(all_ssreflect) extra