proposition: Lemma index_enum_uniq T : uniq (index_enum T).
proof: Proof. by rewrite [index_enum T]unlock -enumT enum_uniq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)