proposition: Lemma add_1 : forall e s, mem e (add e s).
proof: Proof. intros e s; unfold mem, add; simpl; destruct (In_dec eq_elt_dec e (support s)) as [e_in_s | e_not_in_s]. trivial. left; trivial. Qed.
imports: List more_list list_permut Arith