proposition: Lemma add_comm : forall e1 e2 s, eq_set (add e1 (add e2 s)) (add e2 (add e1 s)).
proof: Proof. assert (H : forall e1 e2 s, subset (add e1 (add e2 s)) (add e2 (add e1 s))). intros e1 e2 s e; intro H. destruct (add_12 _ _ _ H) as [e_eq_e1 | e_in_e2_s]. unfold mem; apply (mem_eq_mem eq_proof e1). apply (equiv_sym _ _ eq_proof); assumption. apply add_2; subst; apply add_1. destruct (add_12 _ _ _ e_in_e2_s) as [e_eq_e2 | e_in_s]. unfold mem; apply (mem_eq_mem eq_proof e2). apply (equiv_sym _ _ eq_proof); assumption. apply add_1. do 2 apply add_2; trivial. intros e1 e2 s; split; apply H. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)