proposition: Lemma deprecated_filter_index_enum T P : filter P (index_enum T) = enum P.
proof: Proof. by rewrite [index_enum T]unlock. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)