proposition: Lemma card_ffun_on R : #|@ffun_on aT R| = #|R| ^ #|aT|.
proof: Proof. rewrite card_family /image_mem cardT. by elim: (enum aT) => //= _ e ->; rewrite expnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)