fact: Fixpoint without_red_bool (l : list A) {struct l} : bool := match l with | nil => true | e :: le => if (mem_bool eq_bool e le) then false else without_red_bool le end.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)