proposition: Lemma card_pffun_on y0 D R : #|pffun_on y0 D R| = #|R| ^ #|D|.
proof: Proof. rewrite (cardE D) card_pfamily /image_mem. by elim: (enum D) => //= _ e ->; rewrite expnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)