fact: Definition filter (P_bool : A -> bool) s (P_compat : forall e e', eq_A e e' -> (P_bool e = P_bool e')) := mk_set (without_red_filter_aux P_bool s.(is_a_set)).
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)