proposition: Lemma enum_fsetT {I : finType} : perm_eq (enum [fset i | i in I]) (enum I).
proof: Proof. apply/uniq_perm; rewrite ?enum_uniq //. by move=> i /=; rewrite !mem_enum in_imfset. Qed.
imports: mathcomp(all_ssreflect all_algebra)