proposition: Lemma add_in : forall (A : part_set E) (x : E), in_part x A -> Equal (add_part A x) A.
proof: Proof. intro A. case A. simpl in |- *; unfold pred_compatible, eq_part, in_part in |- *; simpl in |- *. intuition eauto. Qed.
imports: Union Singleton Diff Classical_Prop