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