proposition: Lemma card_pfamily y0 D F : #|pfamily y0 D F| = foldr muln 1 [seq #|F x| | x in D].
proof: Proof. rewrite card_family !/(image _ _) /(enum D) -enumT /=. by elim: (enum aT) => //= x E ->; have [// | D'x] := ifP; rewrite card1 mul1n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)