proposition: Lemma add_2 : forall e e' s, mem e s -> mem e (add e' s).
proof: Proof. intros e e' s; unfold mem, add; simpl; destruct (In_dec eq_elt_dec e' (support s)) as [e'_in_s | e'_not_in_s]. trivial. right; trivial. Qed.
imports: List more_list list_permut Arith