proposition: Lemma add_12 : forall e e' s, mem e (add e' s) -> e = e' \/ mem 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]. right; trivial. intros [e'_eq_e | e_in_s]; [left; subst | right]; trivial. Qed.
imports: List more_list list_permut Arith