proposition: Lemma enum_fset1 (T : choiceType) (x : T) : enum ([fset x] : finType) = [:: [`fset11 x]].
proof: Proof. apply/perm_small_eq=> //; apply/uniq_perm => //. by apply/enum_uniq. case=> [y hy]; rewrite mem_seq1 mem_enum /in_mem /=. by rewrite eqE /=; rewrite in_fset1 in hy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)