proposition: Lemma empty_not_in : forall A : part_set E, Equal A (empty E) -> forall x : E, ~ in_part x A.
proof: Proof. intros A; case A; intros a pa; simpl in |- *. unfold eq_part, empty in |- *; simpl in |- *. intuition. intros. elim (H x); auto with *. Qed.
imports: Fpart Inter Arith