fact: Fixpoint add_without_red (acc l : list elt) {struct l} : list elt := match l with | nil => acc | e :: le => if (In_dec eq_elt_dec e acc) then add_without_red acc le else add_without_red (e :: acc) le end.
imports: List more_list list_permut Arith