proposition: Lemma without_red_singleton : forall e : A, without_red (e :: nil).
proof: Proof. unfold without_red; intro e; simpl; reflexivity. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)