proposition: Lemma eq_set_dec : forall s1 s2, {eq_set s1 s2} + {~eq_set s1 s2}.
proof: Proof. intros s1 s2; destruct (subset_dec s1 s2) as [ s1_incl_s2 | s1_not_incl_s2 ]. destruct (subset_dec s2 s1) as [ s2_incl_s1 | s2_not_incl_s1 ]. left; intro e; intuition. right; intro s1_eq_s2; apply s2_not_incl_s1; intros e e_in_s2; generalize (s1_eq_s2 e); intuition. right; intro s1_eq_s2; apply s1_not_incl_s2; intros e e_in_s1; generalize (s1_eq_s2 e); intuition. Qed.
imports: List more_list list_permut Arith