proposition: Lemma not_in_empty : forall A : part_set E, (forall x : E, ~ in_part x A) -> Equal A (empty E).
proof: Proof. intros A. case A. intros a pa. simpl in |- *. unfold eq_part, empty in |- *; simpl in |- *. intuition eauto. Qed.
imports: Union Singleton Diff Classical_Prop