proposition: Lemma without_red_add_without_red : forall l1 l2, without_red l1 -> without_red (add_without_red l1 l2).
proof: Proof. unfold without_red; intros l1 l2 Wl1; functional induction (add_without_red l1 l2) as [ | l1 H1 e l2 H2 e_in_l1 IH | l1 H1 e l2 H2 e_not_in_l1 IH ]. assumption. apply IH; assumption. apply IH; simpl. rewrite e_not_in_l1; assumption. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)