proposition: Lemma empty_inter : forall A : part_set E, Equal (inter (empty E) A) (empty E).
proof: Proof. intros A; try assumption. apply in_eq_part. intros x H'; try assumption. apply in_part_inter_l with A; auto with *. intros x H'; try assumption. absurd (in_part x (empty E)); auto with *. Qed.
imports: Fpart Inter Arith