proposition: Lemma card_uniq_tuples T n (A : pred T) : #|[set t : n.-tuple T | all A t & uniq t]| = #|A| ^_ n.
proof: Proof. elim: n A => [|n IHn] A. by rewrite (@eq_card1 _ [tuple]) // => t; rewrite [t]tuple0 inE. rewrite -sum1dep_card (partition_big (@thead _ _) A) /= => [|t]; last first. by case/tupleP: t => x t; do 2!case/andP. rewrite ffactnS -sum_nat_const; apply: eq_bigr => x Ax. rewrite (cardD1 x) [x \in A]Ax /= -(IHn [predD1 A & x]) -sum1dep_card. rewrite (reindex (fun t : n.-tuple T => [tuple of x :: t])) /=; last first. pose ttail (t : n.+1.-tuple T) := [tuple of behead t]. exists ttail => [t _ | t /andP[_ /eqP <-]]; first exact: val_inj. by rewrite -tuple_eta. apply: eq_bigl=> t; rewrite Ax theadE eqxx andbT /= andbA; congr (_ && _). by rewrite all_predI all_predC has_pred1 andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)