proposition: Lemma card_family (F : forall x, pred (rT x)) : #|(family F : simpl_pred fT)| = foldr muln 1 [seq #|F x| | x : aT].
proof: Proof. rewrite /image_mem; set E := enum aT in (uniqE := enum_uniq aT) *. have trivF x: x \notin E -> #|F x| = 1 by rewrite mem_enum. elim: E uniqE => /= [_ | x0 E IH_E /andP[E'x0 uniqE]] in F trivF *. have /fin_all_exists[f0 Ff0] x: exists y0, F x =i pred1 y0. have /pred0Pn[y Fy]: #|F x| != 0 by rewrite trivF. by exists y; apply/fsym/subset_cardP; rewrite ?subset_pred1 // card1 trivF. apply: eq_card1 (finfun f0 : fT) _ _ => f; apply/familyP/eqP=> [Ff | {f}-> x]. by apply/ffunP=> x; have /[!(Ff0, ffunE)]/eqP := Ff x. by rewrite ffunE Ff0 inE /=. have [y0 Fxy0 | Fx00] := pickP (F x0); last first. by rewrite !eq_card0 // => f; apply: contraFF (Fx00 (f x0))=> /familyP; apply. pose F1 x := if eqP is ReflectT Dx then xpred1 (ecast x (rT x) Dx y0) else F x. transitivity (#|[predX F x0 & family F1 : pred fT]|); last first. rewrite cardX {}IH_E {uniqE}// => [|x E'x]; last first. rewrite /F1; case: eqP => [Dx | /nesym/eqP-x0'x]; first exact: card1. by rewrite trivF // negb_or x0'x. congr (_ * foldr _ _ _); apply/eq_in_map=> x Ex. by rewrite /F1; case: eqP => // Dx0; rewrite Dx0 Ex in E'x0. pose g yf : fT := let: (y, f) := yf : rT x0 * fT in [ffun x => if eqP is ReflectT Dx then ecast x (rT x) Dx y else f x]. have gK: cancel (fun f : fT => (f x0, g (y0, f))) g. by move=> f; apply/ffunP=> x; rewrite !ffunE; case: eqP => //; case: x /. rewrite -(card_image (can_inj gK)); apply: eq_card => [] [y f] /=. apply/imageP/andP=> [[f1 /familyP/=Ff1] [-> ->]| [/=Fx0y /familyP/=Ff]]. split=> //; apply/familyP=> x; rewrite ffunE /F1 /=. by case: eqP => // Dx; apply: eqxx. exists (g (y, f)). by apply/familyP=> x; have:= Ff x; rewrite ffunE /F1; case: eqP; [case: x /|]. congr (_, _); first by rewrite /= ffunE; case: eqP => // Dx; rewrite eq_axiomK. by apply/ffunP=> x; have:= Ff x; rewrite !ffunE /F1; case: eqP => // Dx /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)