proposition: Lemma add_prf : forall e l, without_red l -> ~In e l -> without_red (e :: l).
proof: Proof. intros e l Wl e_not_in_l; simpl; destruct (In_dec eq_elt_dec e l) as [e_in_l | _]; trivial; apply e_not_in_l; trivial. Qed.
imports: List more_list list_permut Arith