proposition: Lemma union_assoc : forall A B C : part_set E, Equal (union A (union B C)) (union (union A B) C).
proof: Proof. unfold union in |- *; simpl in |- *. unfold eq_part in |- *; simpl in |- *. intros A B C x; split; [ try assumption | idtac ]. intuition. intuition. Qed.
imports: Parts