proposition: Lemma add_compat_eq_set : forall e s1 s2, eq_set s1 s2 -> eq_set (add e s1) (add e s2).
proof: Proof. assert (forall a e s1 s2, eq_set s1 s2 -> mem a (add e s1) -> mem a (add e s2)). intros a e s1 s2 s1_eq_s2 a_mem_e_s1. destruct (add_12 _ _ _ a_mem_e_s1) as [a_eq_e | a_mem_s1]. assert (e_eq_a : EDS1.eq_A e a). symmetry; trivial. apply (eq_mem_mem (add e s2) e_eq_a). apply add_1. apply add_2; rewrite <- (s1_eq_s2 a); trivial. intros e s1 s2 s1_eq_s2 a; split; apply H; trivial. apply eq_set_sym; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)