proposition: Lemma set0X (A B : finType) (F : {set B}) : set0 `* F = set0 :> {set A * B}.
proof: Proof. by apply/setP/subset_eqP/andP; split; apply/subsetP => -[a b]; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect fingroup perm)