proposition: Lemma in_eq_part : forall A B : part_set E, (forall x : E, in_part x A -> in_part x B) -> (forall x : E, in_part x B -> in_part x A) -> Equal A B.
proof: Proof. intros A B. case A; case B; simpl in |- *. intros a pa b pb. unfold eq_part in |- *; simpl in |- *. intuition. Qed.
imports: Fpart Inter Arith