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