fact: Definition setXn n (fT : 'I_n -> finType) (A : forall i, {set fT i}) : {set {dffun forall i, fT i}} := [set x : {dffun forall i, fT i} | [forall i : 'I_n, x i \in A i]].
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)