proposition: Lemma in_part_comp_r : forall (x : E) (A B : part_set E), in_part x A -> Equal A B -> in_part x B.
proof: Proof. simpl in |- *; unfold eq_part in |- *. intros x A B H' H'0; try assumption. elim (H'0 x). intuition. Qed.
imports: Sets