proposition: Lemma filter_index_enum : forall T P, filter P (index_enum T) = enum P.
proof: Proof. by []. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops