proposition: Lemma union_comm : forall s1 s2, eq_set (union s1 s2) (union s2 s1).
proof: Proof. intros s1 s2 e; generalize (union_12 s1 s2 e) (union_1 s1 s2 e) (union_2 s1 s2 e) (union_12 s2 s1 e) (union_1 s2 s1 e) (union_2 s2 s1 e); intuition. Qed.
imports: List more_list list_permut Arith