proposition: Lemma union_diff : forall A B : part_set E, Equal (union A (diff B A)) (union A B).
proof: Proof. intros A B; try assumption. apply in_eq_part. intros x H'; try assumption. elim (in_part_union H'). auto with *. intros H'0; try assumption. cut (in_part x B). auto with *. exact (diff_in_l H'0). intros x H'; try assumption. elim (in_part_union H'). auto with *. intros H'0; try assumption. elim (classic (in_part x A)). auto with *. intros H'1; try assumption. cut (in_part x (diff B A)). auto with *. auto with *. Qed.
imports: Fpart Inter Arith