proposition: Lemma fset1_inj : injective (@fset1 K).
proof: Proof. by move=> a b eqsab; apply/fset1P; rewrite -eqsab fset11. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)