proposition: Lemma remove_red_included : forall e l, In e l -> In e (remove_red l).
proof: Proof. intros x l; induction l as [ | e le ]. contradiction. intros [x_eq_e | x_in_le]; simpl. subst x; destruct (In_dec eq_elt_dec e le) as [ in_e_le | not_in_e_le]; [ apply IHle | left ]; trivial. destruct (In_dec eq_elt_dec e le) as [ in_e_le | not_in_e_le]; [ idtac | right]; apply IHle; trivial. Qed.
imports: List more_list list_permut Arith